Metamath Proof Explorer

Theorem elsymdif

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

Ref Expression
Assertion elsymdif ⊢ A ∈ B ∆ C ↔ ¬ A ∈ B ↔ A ∈ C

Proof

Step Hyp Ref Expression
1 elun ⊢ A ∈ B ∖ C ∪ C ∖ B ↔ A ∈ B ∖ C ∨ A ∈ C ∖ B
2 eldif ⊢ A ∈ B ∖ C ↔ A ∈ B ∧ ¬ A ∈ C
3 eldif ⊢ A ∈ C ∖ B ↔ A ∈ C ∧ ¬ A ∈ B
4 2 3 orbi12i ⊢ A ∈ B ∖ C ∨ A ∈ C ∖ B ↔ A ∈ B ∧ ¬ A ∈ C ∨ A ∈ C ∧ ¬ A ∈ B
5 1 4 bitri ⊢ A ∈ B ∖ C ∪ C ∖ B ↔ A ∈ B ∧ ¬ A ∈ C ∨ A ∈ C ∧ ¬ A ∈ B
6 df-symdif ⊢ B ∆ C = B ∖ C ∪ C ∖ B
7 6 eleq2i ⊢ A ∈ B ∆ C ↔ A ∈ B ∖ C ∪ C ∖ B
8 xor ⊢ ¬ A ∈ B ↔ A ∈ C ↔ A ∈ B ∧ ¬ A ∈ C ∨ A ∈ C ∧ ¬ A ∈ B
9 5 7 8 3bitr4i ⊢ A ∈ B ∆ C ↔ ¬ A ∈ B ↔ A ∈ C