This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ( 𝐵 △ 𝐶 ) ↔ ¬ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶 ) )