Theorem cnv0 6159

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5295, ax-nul 5305, ax-pr 5431. (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 5191	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 486	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1799	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1799	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5692	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6		df-opab 5205	. . . . 5 ⊢ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
7	5, 6	eqtri 2764	. . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
8	7	eqabri 2884	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	4, 8	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
10	9	nel0 4353	1 ⊢ ◡∅ = ∅

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2713  ∅c0 4332  ⟨cop 4631   class class class wbr 5142  {copab 5204  ^◡ccnv 5683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-dif 3953  df-nul 4333  df-br 5143  df-opab 5205  df-cnv 5692

This theorem is referenced by:  xp0  6177  cnveq0  6216  co01  6280  funcnv0  6631  f1o00  6882  tpos0  8282  cnvfi  9217  oduleval  18335  ust0  24229  nghmfval  24744  isnghm  24745  1pthdlem1  30155  mptiffisupp  32703  tocycf  33138  tocyc01  33139  mthmval  35581  resnonrel  43610  cononrel1  43612  cononrel2  43613  cnvrcl0  43643  0cnf  45897