Theorem cnv0 6098

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5261, ax-nul 5268, ax-pr 5389. (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 5159	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 487	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1802	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1802	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5646	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6		df-opab 5173	. . . . 5 ⊢ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
7	5, 6	eqtri 2759	. . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
8	7	eqabri 2876	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	4, 8	mtbir 322	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
10	9	nel0 4315	1 ⊢ ◡∅ = ∅

Syntax hints:   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2708  ∅c0 4287  ⟨cop 4597   class class class wbr 5110  {copab 5172  ^◡ccnv 5637

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-dif 3916  df-nul 4288  df-br 5111  df-opab 5173  df-cnv 5646

This theorem is referenced by:  xp0  6115  cnveq0  6154  co01  6218  funcnv0  6572  f1o00  6824  tpos0  8192  cnvfi  9131  oduleval  18192  ust0  23608  nghmfval  24123  isnghm  24124  1pthdlem1  29142  mptiffisupp  31675  tocycf  32036  tocyc01  32037  mthmval  34256  resnonrel  41986  cononrel1  41988  cononrel2  41989  cnvrcl0  42019  0cnf  44238