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