Theorem cnv0 6101

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5246, ax-nul 5256, ax-pr 5382. (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 5151	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 486	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1800	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1800	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5639	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6		df-opab 5165	. . . . 5 ⊢ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
7	5, 6	eqtri 2752	. . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
8	7	eqabri 2871	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	4, 8	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
10	9	nel0 4313	1 ⊢ ◡∅ = ∅

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  ∅c0 4292  ⟨cop 4591   class class class wbr 5102  {copab 5164  ^◡ccnv 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3914  df-nul 4293  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  xp0  6119  cnveq0  6158  co01  6222  funcnv0  6566  f1o00  6817  tpos0  8212  cnvfi  9117  oduleval  18230  ust0  24140  nghmfval  24643  isnghm  24644  1pthdlem1  30114  mptiffisupp  32666  tocycf  33089  tocyc01  33090  mthmval  35555  resnonrel  43574  cononrel1  43576  cononrel2  43577  cnvrcl0  43607  0cnf  45868