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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 △ 𝐵 ) △ 𝐶 ) = ( 𝐴 △ ( 𝐵 △ 𝐶 ) )