Theorem cnv0 5984

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5177, ax-nul 5184, ax-pr 5307. (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 5088	. . . . . 6 ⊢ ¬ 𝑦∅𝑧
2	1	intnan 490	. . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
3	2	nex 1808	. . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
4	3	nex 1808	. . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)
5		df-cnv 5544	. . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧}
6		df-opab 5102	. . . . 5 ⊢ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
7	5, 6	eqtri 2759	. . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)}
8	7	abeq2i 2865	. . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧))
9	4, 8	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ◡∅
10	9	nel0 4251	1 ⊢ ◡∅ = ∅

Syntax hints:   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2112  {cab 2714  ∅c0 4223  ⟨cop 4533   class class class wbr 5039  {copab 5101  ^◡ccnv 5535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-dif 3856  df-nul 4224  df-br 5040  df-opab 5102  df-cnv 5544

This theorem is referenced by:  xp0  6001  cnveq0  6040  co01  6105  funcnv0  6424  f1o00  6673  tpos0  7976  cnvfi  8834  oduleval  17751  ust0  23071  nghmfval  23574  isnghm  23575  1pthdlem1  28172  tocycf  31057  tocyc01  31058  mthmval  33204  resnonrel  40817  cononrel1  40819  cononrel2  40820  cnvrcl0  40850  0cnf  43036