Theorem symdifeq1

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

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

Proof

Step	Hyp	Ref	Expression
1		difeq1	|- ( A = B -> ( A \ C ) = ( B \ C ) )
2		difeq2	|- ( A = B -> ( C \ A ) = ( C \ B ) )
3	1 2	uneq12d	|- ( A = B -> ( ( A \ C ) u. ( C \ A ) ) = ( ( B \ C ) u. ( C \ B ) ) )
4		df-symdif	|- ( A /_\ C ) = ( ( A \ C ) u. ( C \ A ) )
5		df-symdif	|- ( B /_\ C ) = ( ( B \ C ) u. ( C \ B ) )
6	3 4 5	3eqtr4g	|- ( A = B -> ( A /_\ C ) = ( B /_\ C ) )