Metamath Proof Explorer

Definition df-nelbr

Description: Define negated membership as binary relation. Analogous to df-eprel (the membership relation). (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion df-nelbr 
|- e// = { <. x , y >. | -. x e. y }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnelbr 
 |-  e//
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 2 cv 
 |-  y
5 3 4 wcel 
 |-  x e. y
6 5 wn 
 |-  -. x e. y
7 6 1 2 copab 
 |-  { <. x , y >. | -. x e. y }
8 0 7 wceq 
 |-  e// = { <. x , y >. | -. x e. y }