Theorem elsymdif

Description: Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	elsymdif	⊢ ( 𝐴 ∈ ( 𝐵 △ 𝐶 ) ↔ ¬ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elun	⊢ ( 𝐴 ∈ ( ( 𝐵 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐵 ) ) ↔ ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ∨ 𝐴 ∈ ( 𝐶 ∖ 𝐵 ) ) )
2		eldif	⊢ ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) )
3		eldif	⊢ ( 𝐴 ∈ ( 𝐶 ∖ 𝐵 ) ↔ ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐴 ∈ 𝐵 ) )
4	2 3	orbi12i	⊢ ( ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ∨ 𝐴 ∈ ( 𝐶 ∖ 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ∨ ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐴 ∈ 𝐵 ) ) )
5	1 4	bitri	⊢ ( 𝐴 ∈ ( ( 𝐵 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ∨ ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐴 ∈ 𝐵 ) ) )
6		df-symdif	⊢ ( 𝐵 △ 𝐶 ) = ( ( 𝐵 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐵 ) )
7	6	eleq2i	⊢ ( 𝐴 ∈ ( 𝐵 △ 𝐶 ) ↔ 𝐴 ∈ ( ( 𝐵 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐵 ) ) )
8		xor	⊢ ( ¬ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶 ) ↔ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ∨ ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐴 ∈ 𝐵 ) ) )
9	5 7 8	3bitr4i	⊢ ( 𝐴 ∈ ( 𝐵 △ 𝐶 ) ↔ ¬ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶 ) )