Metamath Proof Explorer

Theorem dfdif3

Description: Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022) (Proof shortened by SN, 15-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 dfdif2 
 |-  ( A \ B ) = { x e. A | -. x e. B }
2 nelb 
 |-  ( -. x e. B <-> A. y e. B y =/= x )
3 necom 
 |-  ( y =/= x <-> x =/= y )
4 3 ralbii 
 |-  ( A. y e. B y =/= x <-> A. y e. B x =/= y )
5 2 4 bitri 
 |-  ( -. x e. B <-> A. y e. B x =/= y )
6 1 5 rabbieq 
 |-  ( A \ B ) = { x e. A | A. y e. B x =/= y }