Metamath Proof Explorer

Theorem elsymdif

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

Ref Expression
Assertion elsymdif 
|- ( A e. ( B /_\ C ) <-> -. ( A e. B <-> A e. C ) )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( A e. ( ( B \ C ) u. ( C \ B ) ) <-> ( A e. ( B \ C ) \/ A e. ( C \ B ) ) )
2 eldif 
 |-  ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
3 eldif 
 |-  ( A e. ( C \ B ) <-> ( A e. C /\ -. A e. B ) )
4 2 3 orbi12i 
 |-  ( ( A e. ( B \ C ) \/ A e. ( C \ B ) ) <-> ( ( A e. B /\ -. A e. C ) \/ ( A e. C /\ -. A e. B ) ) )
5 1 4 bitri 
 |-  ( A e. ( ( B \ C ) u. ( C \ B ) ) <-> ( ( A e. B /\ -. A e. C ) \/ ( A e. C /\ -. A e. B ) ) )
6 df-symdif 
 |-  ( B /_\ C ) = ( ( B \ C ) u. ( C \ B ) )
7 6 eleq2i 
 |-  ( A e. ( B /_\ C ) <-> A e. ( ( B \ C ) u. ( C \ B ) ) )
8 xor 
 |-  ( -. ( A e. B <-> A e. C ) <-> ( ( A e. B /\ -. A e. C ) \/ ( A e. C /\ -. A e. B ) ) )
9 5 7 8 3bitr4i 
 |-  ( A e. ( B /_\ C ) <-> -. ( A e. B <-> A e. C ) )