Metamath Proof Explorer

Theorem nelbr

Description: The binary relation of a set not being a member of another set. (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion nelbr 
|- ( ( A e. V /\ B e. W ) -> ( A e// B <-> -. A e. B ) )

Proof

Step Hyp Ref Expression
1 eleq12 
 |-  ( ( x = A /\ y = B ) -> ( x e. y <-> A e. B ) )
2 1 notbid 
 |-  ( ( x = A /\ y = B ) -> ( -. x e. y <-> -. A e. B ) )
3 df-nelbr 
 |-  e// = { <. x , y >. | -. x e. y }
4 2 3 brabga 
 |-  ( ( A e. V /\ B e. W ) -> ( A e// B <-> -. A e. B ) )