Metamath Proof Explorer

Theorem cnvepnep

Description: The membership (epsilon) relation and its converse are disjoint, i.e., _E is an asymmetric relation. Variable-free version of en2lp . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022)

Ref Expression
Assertion cnvepnep 
|- ( `' _E i^i _E ) = (/)

Proof

Step Hyp Ref Expression
1 df-eprel 
 |-  _E = { <. y , x >. | y e. x }
2 1 cnveqi 
 |-  `' _E = `' { <. y , x >. | y e. x }
3 cnvopab 
 |-  `' { <. y , x >. | y e. x } = { <. x , y >. | y e. x }
4 2 3 eqtri 
 |-  `' _E = { <. x , y >. | y e. x }
5 df-eprel 
 |-  _E = { <. x , y >. | x e. y }
6 4 5 ineq12i 
 |-  ( `' _E i^i _E ) = ( { <. x , y >. | y e. x } i^i { <. x , y >. | x e. y } )
7 inopab 
 |-  ( { <. x , y >. | y e. x } i^i { <. x , y >. | x e. y } ) = { <. x , y >. | ( y e. x /\ x e. y ) }
8 6 7 eqtri 
 |-  ( `' _E i^i _E ) = { <. x , y >. | ( y e. x /\ x e. y ) }
9 en2lp 
 |-  -. ( y e. x /\ x e. y )
10 9 gen2 
 |-  A. x A. y -. ( y e. x /\ x e. y )
11 opab0 
 |-  ( { <. x , y >. | ( y e. x /\ x e. y ) } = (/) <-> A. x A. y -. ( y e. x /\ x e. y ) )
12 10 11 mpbir 
 |-  { <. x , y >. | ( y e. x /\ x e. y ) } = (/)
13 8 12 eqtri 
 |-  ( `' _E i^i _E ) = (/)