Theorem cnvepnep

Description: The membership (epsilon) relation and its converse are disjoint, i.e., _E is an asymmetric relation. Variable-free version of en2lp . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022)

	Ref	Expression
Assertion	cnvepnep	$$⊢{\mathrm{E}}^{-1}\cap \mathrm{E}=\varnothing$$

Proof

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