Theorem

Let A be an object. Let φ(a) be a proposition depending on a member a of A. Assume ∃a∈A⋅φ(a) and {a∈A|φ(a)}=∅. Then we have false.

Background

The following background is necessary to understand this theorem.

(.) Let A and x be objects. Then x∈A is a proposition.

(.) Let x and y be objects. Then x=y is a proposition.

(.) ∅ is an object.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then {a∈A|φ(a)} is an object.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then "∃a∈A⋅φ(a)" is a proposition.

(.) "false" is a proposition.

Background for Proof

The following background is necessary for the proof.

(.) Let x and y be objects. Let φ(x) be a proposition depending on an object x. Assume x=y and φ(x). Then we know φ(y).

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Let a be a member of A. Assume φ(a). Then we know a∈{a∈A|φ(a)}.

(.) Let x be an object. Assume x∈∅. Let φ be a proposition. Then we know φ.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Assume ∃a∈A⋅φ(a). Let ψ be a proposition. Assume for all a ∈ A φ(a) implies ψ. Then we know ψ.

Proof

Let a be a member of A such that φ(a). We will show a∈∅. Since φ(a), we know a∈{a∈A|φ(a)}. Using this and {a∈A|φ(a)}=∅, we are done.

Click here to modify variable names (JavaScript Must Be Enabled).