Theorem cnv0 5857

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5248, ax-nul 5259, ax-pr 5390. (Revised by KP, 25-Oct-2021.) Avoid ax-12 2213. (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 5153	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 492	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1833	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1833	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5655	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6	5	eleq2i 2852	. . . 4 ⊢ (𝑥 ∈ ◡∅ ↔ 𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧})
7		elopabw 5496	. . . . 5 ⊢ (𝑥 ∈ V → (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)))
8	7	elv 3455	. . . 4 ⊢ (𝑥 ∈ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	6, 8	bitri 278	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
10	4, 9	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
11	10	nel0 4301	1 ⊢ ◡∅ = ∅

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3450  ∅c0 4278  ⟨cop 4589   class class class wbr 5102  {copab 5166  ^◡ccnv 5646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3901  df-nul 4279  df-br 5103  df-opab 5167  df-cnv 5655

This theorem is used by:  csbcnv  5860  xp0OLD  6144  cnveq0  6185  co01  6252  funcnv0  6594  f1o00  6848  tpos0  8251  cnvfi  9169  oduleval  18424  ust0  24500  nghmfval  25002  isnghm  25003  1pthdlem1  30659  mptiffisupp  33219  tocycf  33611  tocyc01  33612  vieta  34145  mthmval  36261  resnonrel  44536  cononrel1  44538  cononrel2  44539  cnvrcl0  44569  0cnf  46809