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	⊢ ( 𝐴 △ 𝐵 ) = { 𝑥 ∣ ¬ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) }