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 =

Proof

Step Hyp Ref Expression
1 df-eprel E = x y | x y
2 df-id I = x y | x = y
3 1 2 ineq12i E I = x y | x y x y | x = y
4 inopab x y | x y x y | x = y = x y | x y x = y
5 nelaneq ¬ x y x = y
6 5 gen2 x y ¬ x y x = y
7 opab0 x y | x y x = y = x y ¬ x y x = y
8 6 7 mpbir x y | x y x = y =
9 3 4 8 3eqtri E I =