Theorem symdifass

Description: Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012) (Proof shortened by BJ, 7-Sep-2022)

	Ref	Expression
Assertion	symdifass	⊢ ( ( 𝐴 △ 𝐵 ) △ 𝐶 ) = ( 𝐴 △ ( 𝐵 △ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elsymdifxor	⊢ ( 𝑥 ∈ ( ( 𝐴 △ 𝐵 ) △ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐴 △ 𝐵 ) ⊻ 𝑥 ∈ 𝐶 ) )
2		elsymdifxor	⊢ ( 𝑥 ∈ ( 𝐴 △ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵 ) )
3		biid	⊢ ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶 )
4	2 3	xorbi12i	⊢ ( ( 𝑥 ∈ ( 𝐴 △ 𝐵 ) ⊻ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵 ) ⊻ 𝑥 ∈ 𝐶 ) )
5		xorass	⊢ ( ( ( 𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵 ) ⊻ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ⊻ ( 𝑥 ∈ 𝐵 ⊻ 𝑥 ∈ 𝐶 ) ) )
6		biid	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 )
7		elsymdifxor	⊢ ( 𝑥 ∈ ( 𝐵 △ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ⊻ 𝑥 ∈ 𝐶 ) )
8	7	bicomi	⊢ ( ( 𝑥 ∈ 𝐵 ⊻ 𝑥 ∈ 𝐶 ) ↔ 𝑥 ∈ ( 𝐵 △ 𝐶 ) )
9	6 8	xorbi12i	⊢ ( ( 𝑥 ∈ 𝐴 ⊻ ( 𝑥 ∈ 𝐵 ⊻ 𝑥 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ ( 𝐵 △ 𝐶 ) ) )
10	4 5 9	3bitri	⊢ ( ( 𝑥 ∈ ( 𝐴 △ 𝐵 ) ⊻ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ ( 𝐵 △ 𝐶 ) ) )
11		elsymdifxor	⊢ ( 𝑥 ∈ ( 𝐴 △ ( 𝐵 △ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ ( 𝐵 △ 𝐶 ) ) )
12	11	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ ( 𝐵 △ 𝐶 ) ) ↔ 𝑥 ∈ ( 𝐴 △ ( 𝐵 △ 𝐶 ) ) )
13	1 10 12	3bitri	⊢ ( 𝑥 ∈ ( ( 𝐴 △ 𝐵 ) △ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 △ ( 𝐵 △ 𝐶 ) ) )
14	13	eqriv	⊢ ( ( 𝐴 △ 𝐵 ) △ 𝐶 ) = ( 𝐴 △ ( 𝐵 △ 𝐶 ) )