Metamath Proof Explorer

Theorem symdifeq2

Description: Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012)

Ref Expression
Assertion symdifeq2 
|- ( A = B -> ( C /_\ A ) = ( C /_\ B ) )

Proof

Step Hyp Ref Expression
1 symdifeq1 
 |-  ( A = B -> ( A /_\ C ) = ( B /_\ C ) )
2 symdifcom 
 |-  ( C /_\ A ) = ( A /_\ C )
3 symdifcom 
 |-  ( C /_\ B ) = ( B /_\ C )
4 1 2 3 3eqtr4g 
 |-  ( A = B -> ( C /_\ A ) = ( C /_\ B ) )