Theorem

Let A, B and x be objects. Assume x∈A⊕B. Let φ be a proposition. Assume x∈A implies ¬x∈B implies φ and ¬x∈A implies x∈B implies φ. Then we have φ.

Background

The following background is necessary to understand this theorem.

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

(.) Let φ be a proposition. Then ¬φ is a proposition.

(.) Let x and y be objects. Then "x⊕y" is an object.

Background for Proof

The following background is necessary for the proof.

(.) Let φ and ψ be propositions. Then φ∨ψ is a proposition.

(.) Let φ and ψ be propositions. Assume φ and ¬φ. Then we know ψ.

(.) 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. Let x be an object. Assume x∈{a∈A|φ(a)}. Then we know x∈A.

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

(.) Let φ and ψ be propositions. Assume φ∨ψ. Let θ be a proposition. Assume φ implies θ and ψ implies θ. Then we know θ.

(.) Let A and B be objects. Then "A∪B" is an object.

(.) Let A, B and x be objects. Assume x∈A∪B. Then we know x∈A∨x∈B.

(.) Let A and B be objects. Then A⊕B is the object given by {x∈A∪B|¬x∈A∨¬x∈B}.

Proof

Claim: ¬x∈A∨¬x∈B.

Proof of Claim: Since x∈A⊕B, we have x∈{x∈A∪B|¬x∈A∨¬x∈B}. Using this, we are done. This completes the proof of the claim.

Consider the case in which ¬x∈A.

Claim: x∈A∨x∈B.

Proof of Claim: It is enough to show x∈A∪B. Since x∈A⊕B, we know x∈{x∈A∪B|¬x∈A∨¬x∈B}. Using this, we are done. This completes the proof of the claim.

Consider the case in which x∈A. Using this and ¬x∈A, we conclude φ.

Consider the case in which x∈B. Using this, ¬x∈A and ¬x∈A implies x∈B implies φ, we conclude φ.

Consider the case in which ¬x∈B.

Claim: x∈A∨x∈B.

Proof of Claim: We will show x∈A∪B. Since x∈A⊕B, we have x∈{x∈A∪B|¬x∈A∨¬x∈B}. Using this, we are done. This completes the proof of the claim.

Consider the case in which x∈A. Using this, x∈A implies ¬x∈B implies φ and ¬x∈B, we conclude φ.

Consider the case in which x∈B. Using this and ¬x∈B, we conclude φ.

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

Hide Background.

Test yourself on this item.