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

Metamath Proof Explorer

Theorem dfsymdif4

Description: Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004) (Revised by AV, 17-Aug-2022)

Ref Expression
Assertion dfsymdif4 ( 𝐴 △ 𝐵 ) = { 𝑥 ∣ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) }

Proof

Step Hyp Ref Expression
1 elsymdif ⊢ ( 𝑥 ∈ ( 𝐴 △ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
2 1 eqabi ⊢ ( 𝐴 △ 𝐵 ) = { 𝑥 ∣ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) }