Theorem cnv0 5999

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5203, ax-nul 5210, ax-pr 5330. (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 5115	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 489	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1801	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1801	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5563	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6		df-opab 5129	. . . . 5 ⊢ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
7	5, 6	eqtri 2844	. . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
8	7	abeq2i 2948	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	4, 8	mtbir 325	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
10	9	nel0 4311	1 ⊢ ◡∅ = ∅

Syntax hints:   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2799  ∅c0 4291  ⟨cop 4573   class class class wbr 5066  {copab 5128  ^◡ccnv 5554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-dif 3939  df-nul 4292  df-br 5067  df-opab 5129  df-cnv 5563

This theorem is referenced by:  xp0  6015  cnveq0  6054  co01  6114  funcnv0  6420  f1o00  6649  tpos0  7922  oduleval  17741  ust0  22828  nghmfval  23331  isnghm  23332  1pthdlem1  27914  tocycf  30759  tocyc01  30760  mthmval  32822  resnonrel  39972  cononrel1  39974  cononrel2  39975  cnvrcl0  40005  0cnf  42180