Theorem cnv0 6113

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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  ∅c0 4296  ⟨cop 4595   class class class wbr 5107  {copab 5169  ^◡ccnv 5637

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 3917  df-nul 4297  df-br 5108  df-opab 5170  df-cnv 5646

This theorem is referenced by:  xp0  6131  cnveq0  6170  co01  6234  funcnv0  6582  f1o00  6835  tpos0  8235  cnvfi  9140  oduleval  18250  ust0  24107  nghmfval  24610  isnghm  24611  1pthdlem1  30064  mptiffisupp  32616  tocycf  33074  tocyc01  33075  mthmval  35562  resnonrel  43581  cononrel1  43583  cononrel2  43584  cnvrcl0  43614  0cnf  45875