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 ) = (/)