Metamath Proof Explorer

Theorem dfdif2

Description: Alternate definition of class difference. (Contributed by NM, 25-Mar-2004)

Ref Expression
Assertion dfdif2 
|- ( A \ B ) = { x e. A | -. x e. B }

Proof

Step Hyp Ref Expression
1 df-dif 
 |-  ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
2 df-rab 
 |-  { x e. A | -. x e. B } = { x | ( x e. A /\ -. x e. B ) }
3 1 2 eqtr4i 
 |-  ( A \ B ) = { x e. A | -. x e. B }