This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem epinid0

Description: The membership relation and the identity relation are disjoint. Variable-free version of nelaneq . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022)

Ref Expression
Assertion epinid0 
|- ( _E i^i _I ) = (/)

Proof

Step Hyp Ref Expression
1 df-eprel 
 |-  _E = { <. x , y >. | x e. y }
2 df-id 
 |-  _I = { <. x , y >. | x = y }
3 1 2 ineq12i 
 |-  ( _E i^i _I ) = ( { <. x , y >. | x e. y } i^i { <. x , y >. | x = y } )
4 inopab 
 |-  ( { <. x , y >. | x e. y } i^i { <. x , y >. | x = y } ) = { <. x , y >. | ( x e. y /\ x = y ) }
5 nelaneq 
 |-  -. ( x e. y /\ x = y )
6 5 gen2 
 |-  A. x A. y -. ( x e. y /\ x = y )
7 opab0 
 |-  ( { <. x , y >. | ( x e. y /\ x = y ) } = (/) <-> A. x A. y -. ( x e. y /\ x = y ) )
8 6 7 mpbir 
 |-  { <. x , y >. | ( x e. y /\ x = y ) } = (/)
9 3 4 8 3eqtri 
 |-  ( _E i^i _I ) = (/)