Metamath Proof Explorer

Theorem dfnelbr2

Description: Alternate definition of the negated membership as binary relation. (Proposed by BJ, 27-Dec-2021.) (Contributed by AV, 27-Dec-2021)

Ref Expression
Assertion dfnelbr2 
|- e// = ( ( _V X. _V ) \ _E )

Proof

Step Hyp Ref Expression
1 difopab 
 |-  ( { <. x , y >. | ( x e. _V /\ y e. _V ) } \ { <. x , y >. | x e. y } ) = { <. x , y >. | ( ( x e. _V /\ y e. _V ) /\ -. x e. y ) }
2 df-xp 
 |-  ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) }
3 df-eprel 
 |-  _E = { <. x , y >. | x e. y }
4 2 3 difeq12i 
 |-  ( ( _V X. _V ) \ _E ) = ( { <. x , y >. | ( x e. _V /\ y e. _V ) } \ { <. x , y >. | x e. y } )
5 df-nelbr 
 |-  e// = { <. x , y >. | -. x e. y }
6 vex 
 |-  x e. _V
7 vex 
 |-  y e. _V
8 6 7 pm3.2i 
 |-  ( x e. _V /\ y e. _V )
9 8 biantrur 
 |-  ( -. x e. y <-> ( ( x e. _V /\ y e. _V ) /\ -. x e. y ) )
10 9 opabbii 
 |-  { <. x , y >. | -. x e. y } = { <. x , y >. | ( ( x e. _V /\ y e. _V ) /\ -. x e. y ) }
11 5 10 eqtri 
 |-  e// = { <. x , y >. | ( ( x e. _V /\ y e. _V ) /\ -. x e. y ) }
12 1 4 11 3eqtr4ri 
 |-  e// = ( ( _V X. _V ) \ _E )