Theorem cnv0 6098

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5242, ax-nul 5252, ax-pr 5378. (Revised by KP, 25-Oct-2021.) Avoid ax-12 2185. (Revised by TM, 31-Jan-2026.)

Assertion

Ref	Expression
cnv0	⊢ ◡∅ = ∅

Proof of Theorem cnv0

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

Step	Hyp	Ref	Expression
1		br0 5148	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 486	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1802	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1802	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5633	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6	5	eleq2i 2829	. . . 4 ⊢ (𝑥 ∈ ◡∅ ↔ 𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧})
7		elopabw 5475	. . . . 5 ⊢ (𝑥 ∈ V → (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)))
8	7	elv 3446	. . . 4 ⊢ (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	6, 8	bitri 275	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
10	4, 9	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
11	10	nel0 4307	1 ⊢ ◡∅ = ∅

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3441  ∅c0 4286  ⟨cop 4587   class class class wbr 5099  {copab 5161  ^◡ccnv 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-dif 3905  df-nul 4287  df-br 5100  df-opab 5162  df-cnv 5633

This theorem is referenced by:  xp0OLD  6117  cnveq0  6156  co01  6221  funcnv0  6559  f1o00  6810  tpos0  8201  cnvfi  9105  oduleval  18217  ust0  24169  nghmfval  24671  isnghm  24672  1pthdlem1  30215  mptiffisupp  32775  tocycf  33203  tocyc01  33204  vieta  33749  mthmval  35782  resnonrel  43911  cononrel1  43913  cononrel2  43914  cnvrcl0  43944  0cnf  46198