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

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 ∪ B ∖ A = B ∖ A ∪ A ∖ B
2 df-symdif ⊢ A ∆ B = A ∖ B ∪ B ∖ A
3 df-symdif ⊢ B ∆ A = B ∖ A ∪ A ∖ B
4 1 2 3 3eqtr4i ⊢ A ∆ B = B ∆ A