Metamath Proof Explorer

Theorem difeq2

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

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

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( A = B -> ( x e. A <-> x e. B ) )
2 1 notbid 
 |-  ( A = B -> ( -. x e. A <-> -. x e. B ) )
3 2 rabbidv 
 |-  ( A = B -> { x e. C | -. x e. A } = { x e. C | -. x e. B } )
4 dfdif2 
 |-  ( C \ A ) = { x e. C | -. x e. A }
5 dfdif2 
 |-  ( C \ B ) = { x e. C | -. x e. B }
6 3 4 5 3eqtr4g 
 |-  ( A = B -> ( C \ A ) = ( C \ B ) )