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 
|- ( ( A /_\ B ) /_\ C ) = ( A /_\ ( B /_\ C ) )

Proof

Step Hyp Ref Expression
1 elsymdifxor 
 |-  ( x e. ( ( A /_\ B ) /_\ C ) <-> ( x e. ( A /_\ B ) \/_ x e. C ) )
2 elsymdifxor 
 |-  ( x e. ( A /_\ B ) <-> ( x e. A \/_ x e. B ) )
3 biid 
 |-  ( x e. C <-> x e. C )
4 2 3 xorbi12i 
 |-  ( ( x e. ( A /_\ B ) \/_ x e. C ) <-> ( ( x e. A \/_ x e. B ) \/_ x e. C ) )
5 xorass 
 |-  ( ( ( x e. A \/_ x e. B ) \/_ x e. C ) <-> ( x e. A \/_ ( x e. B \/_ x e. C ) ) )
6 biid 
 |-  ( x e. A <-> x e. A )
7 elsymdifxor 
 |-  ( x e. ( B /_\ C ) <-> ( x e. B \/_ x e. C ) )
8 7 bicomi 
 |-  ( ( x e. B \/_ x e. C ) <-> x e. ( B /_\ C ) )
9 6 8 xorbi12i 
 |-  ( ( x e. A \/_ ( x e. B \/_ x e. C ) ) <-> ( x e. A \/_ x e. ( B /_\ C ) ) )
10 4 5 9 3bitri 
 |-  ( ( x e. ( A /_\ B ) \/_ x e. C ) <-> ( x e. A \/_ x e. ( B /_\ C ) ) )
11 elsymdifxor 
 |-  ( x e. ( A /_\ ( B /_\ C ) ) <-> ( x e. A \/_ x e. ( B /_\ C ) ) )
12 11 bicomi 
 |-  ( ( x e. A \/_ x e. ( B /_\ C ) ) <-> x e. ( A /_\ ( B /_\ C ) ) )
13 1 10 12 3bitri 
 |-  ( x e. ( ( A /_\ B ) /_\ C ) <-> x e. ( A /_\ ( B /_\ C ) ) )
14 13 eqriv 
 |-  ( ( A /_\ B ) /_\ C ) = ( A /_\ ( B /_\ C ) )