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
dfsymdif2
Next ⟩
symdifass
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfsymdif2
Description:
Alternate definition of the symmetric difference.
(Contributed by
BJ
, 30-Apr-2020)
Ref
Expression
Assertion
dfsymdif2
⊢
A
∆
B
=
x
|
x
∈
A
⊻
x
∈
B
Proof
Step
Hyp
Ref
Expression
1
elsymdifxor
⊢
x
∈
A
∆
B
↔
x
∈
A
⊻
x
∈
B
2
1
abbi2i
⊢
A
∆
B
=
x
|
x
∈
A
⊻
x
∈
B