Metamath Proof Explorer

Theorem symdifcom

Description: Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012)

Ref Expression
Assertion symdifcom 
|- ( A /_\ B ) = ( B /_\ A )

Proof

Step Hyp Ref Expression
1 uncom 
 |-  ( ( A \ B ) u. ( B \ A ) ) = ( ( B \ A ) u. ( A \ B ) )
2 df-symdif 
 |-  ( A /_\ B ) = ( ( A \ B ) u. ( B \ A ) )
3 df-symdif 
 |-  ( B /_\ A ) = ( ( B \ A ) u. ( A \ B ) )
4 1 2 3 3eqtr4i 
 |-  ( A /_\ B ) = ( B /_\ A )