Theorem cnv0 5827

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5220, ax-nul 5230, ax-pr 5364. (Revised by KP, 25-Oct-2021.) Avoid ax-12 2191. (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 5123	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 488	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1808	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1808	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5628	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6	5	eleq2i 2833	. . . 4 ⊢ (𝑥 ∈ ◡∅ ↔ 𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧})
7		elopabw 5470	. . . . 5 ⊢ (𝑥 ∈ V → (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)))
8	7	elv 3438	. . . 4 ⊢ (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	6, 8	bitri 277	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
10	4, 9	mtbir 325	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
11	10	nel0 4284	1 ⊢ ◡∅ = ∅

Syntax hints:   ↔ wb 208   ∧ wa 397   = wceq 1548  ∃wex 1787   ∈ wcel 2121  Vcvv 3433  ∅c0 4263  ⟨cop 4563   class class class wbr 5074  {copab 5136  ^◡ccnv 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3887  df-nul 4264  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  csbcnv  5830  xp0OLD  6112  cnveq0  6151  co01  6216  funcnv0  6554  f1o00  6805  tpos0  8198  cnvfi  9104  oduleval  18250  ust0  24206  nghmfval  24708  isnghm  24709  1pthdlem1  30225  mptiffisupp  32787  tocycf  33200  tocyc01  33201  vieta  33774  mthmval  35816  resnonrel  44049  cononrel1  44051  cononrel2  44052  cnvrcl0  44082  0cnf  46332