Theorem cnvepnep 9619

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

Assertion

Ref	Expression
cnvepnep	⊢ (◡ E ∩ E ) = ∅

Proof of Theorem cnvepnep

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-eprel 5554	. . . . . 6 ⊢ E = {⟨𝑦, 𝑥⟩ ∣ 𝑦 ∈ 𝑥}
2	1	cnveqi 5856	. . . . 5 ⊢ ◡ E = ◡{⟨𝑦, 𝑥⟩ ∣ 𝑦 ∈ 𝑥}
3		cnvopab 6136	. . . . 5 ⊢ ◡{⟨𝑦, 𝑥⟩ ∣ 𝑦 ∈ 𝑥} = {⟨𝑥, 𝑦⟩ ∣ 𝑦 ∈ 𝑥}
4	2, 3	eqtri 2786	. . . 4 ⊢ ◡ E = {⟨𝑥, 𝑦⟩ ∣ 𝑦 ∈ 𝑥}
5		df-eprel 5554	. . . 4 ⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
6	4, 5	ineq12i 4117	. . 3 ⊢ (◡ E ∩ E ) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦 ∈ 𝑥} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦})
7		inopab 5811	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦 ∈ 𝑥} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)}
8	6, 7	eqtri 2786	. 2 ⊢ (◡ E ∩ E ) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)}
9		en2lp 9617	. . . 4 ⊢ ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)
10	9	gen2 1828	. . 3 ⊢ ∀𝑥∀𝑦 ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)
11		opab0 5532	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)} = ∅ ↔ ∀𝑥∀𝑦 ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))
12	10, 11	mpbir 234	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)} = ∅
13	8, 12	eqtri 2786	1 ⊢ (◡ E ∩ E ) = ∅

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401  ∀wal 1567   = wceq 1569   ∩ cin 4091  ∅c0 4280  {copab 5169   E cep 5553  ^◡ccnv 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-pr 5394  ax-reg 9596

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-eprel 5554  df-fr 5607  df-xp 5660  df-rel 5661  df-cnv 5662

This theorem is used by:  epnsym  9620