Theorem cnv0 6092

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 2184. (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 486	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1802	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1802	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5628	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6	5	eleq2i 2827	. . . 4 ⊢ (𝑥 ∈ ◡∅ ↔ 𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧})
7		elopabw 5470	. . . . 5 ⊢ (𝑥 ∈ V → (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)))
8	7	elv 3432	. . . 4 ⊢ (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	6, 8	bitri 275	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
10	4, 9	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
11	10	nel0 4284	1 ⊢ ◡∅ = ∅

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3427  ∅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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

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 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-dif 3888  df-nul 4264  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  xp0OLD  6111  cnveq0  6150  co01  6215  funcnv0  6553  f1o00  6804  tpos0  8195  cnvfi  9099  oduleval  18244  ust0  24173  nghmfval  24675  isnghm  24676  1pthdlem1  30193  mptiffisupp  32754  tocycf  33166  tocyc01  33167  vieta  33712  mthmval  35745  resnonrel  44007  cononrel1  44009  cononrel2  44010  cnvrcl0  44040  0cnf  46293