Theorem cnv0 6033

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5218, ax-nul 5225, ax-pr 5347. (Revised by KP, 25-Oct-2021.)

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 5119	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 486	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1804	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1804	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5588	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6		df-opab 5133	. . . . 5 ⊢ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
7	5, 6	eqtri 2766	. . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
8	7	abeq2i 2874	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	4, 8	mtbir 322	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
10	9	nel0 4281	1 ⊢ ◡∅ = ∅

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  ∅c0 4253  ⟨cop 4564   class class class wbr 5070  {copab 5132  ^◡ccnv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-dif 3886  df-nul 4254  df-br 5071  df-opab 5133  df-cnv 5588

This theorem is referenced by:  xp0  6050  cnveq0  6089  co01  6154  funcnv0  6484  f1o00  6734  tpos0  8043  cnvfi  8924  oduleval  17923  ust0  23279  nghmfval  23792  isnghm  23793  1pthdlem1  28400  tocycf  31286  tocyc01  31287  mthmval  33437  resnonrel  41089  cononrel1  41091  cononrel2  41092  cnvrcl0  41122  0cnf  43308