Metamath Proof Explorer

Theorem difeq1

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion difeq1 
|- ( A = B -> ( A \ C ) = ( B \ C ) )

Proof

Step Hyp Ref Expression
1 rabeq 
 |-  ( A = B -> { x e. A | -. x e. C } = { x e. B | -. x e. C } )
2 dfdif2 
 |-  ( A \ C ) = { x e. A | -. x e. C }
3 dfdif2 
 |-  ( B \ C ) = { x e. B | -. x e. C }
4 1 2 3 3eqtr4g 
 |-  ( A = B -> ( A \ C ) = ( B \ C ) )