Metamath Proof Explorer


Theorem dfdif2

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

Ref Expression
Assertion dfdif2 AB=xA|¬xB

Proof

Step Hyp Ref Expression
1 df-dif AB=x|xA¬xB
2 df-rab xA|¬xB=x|xA¬xB
3 1 2 eqtr4i AB=xA|¬xB