This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The difference, union, and intersection of two classes The symmetric difference of two classes df-symdif
Description: Define the symmetric difference of two classes. Alternate definitions are
dfsymdif2 , dfsymdif3 and dfsymdif4 . (Contributed by Scott Fenton , 31-Mar-2012)
Ref
Expression
Assertion
df-symdif ⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cA ⊢ 𝐴
1
cB ⊢ 𝐵
2
0 1
csymdif ⊢ ( 𝐴 △ 𝐵 )
3
0 1
cdif ⊢ ( 𝐴 ∖ 𝐵 )
4
1 0
cdif ⊢ ( 𝐵 ∖ 𝐴 )
5
3 4
cun ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
6
2 5
wceq ⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )