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	$$⊢\mathrm{E}\cap \mathrm{I}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-eprel	$$⊢\mathrm{E}=\left\{⟨x,y⟩|x\in y\right\}$$
2		df-id	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$
3	1 2	ineq12i	$$⊢\mathrm{E}\cap \mathrm{I}=\left\{⟨x,y⟩|x\in y\right\}\cap \left\{⟨x,y⟩|x=y\right\}$$
4		inopab	$$⊢\left\{⟨x,y⟩|x\in y\right\}\cap \left\{⟨x,y⟩|x=y\right\}=\left\{⟨x,y⟩|\left(x\in y\wedge x=y\right)\right\}$$
5		nelaneq	$$⊢\neg \left(x\in y\wedge x=y\right)$$
6	5	gen2	$$⊢\forall x\forall y\neg \left(x\in y\wedge x=y\right)$$
7		opab0	$$⊢\left\{⟨x,y⟩|\left(x\in y\wedge x=y\right)\right\}=\varnothing \leftrightarrow \forall x\forall y\neg \left(x\in y\wedge x=y\right)$$
8	6 7	mpbir	$$⊢\left\{⟨x,y⟩|\left(x\in y\wedge x=y\right)\right\}=\varnothing$$
9	3 4 8	3eqtri	$$⊢\mathrm{E}\cap \mathrm{I}=\varnothing$$