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