Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnv0 Structured version   Visualization version   GIF version

Theorem cnv0 5966
 Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5167, ax-nul 5174, ax-pr 5295. (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.
StepHypRef Expression
1 br0 5079 . . . . . 6 ¬ 𝑦𝑧
21intnan 490 . . . . 5 ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
32nex 1802 . . . 4 ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
43nex 1802 . . 3 ¬ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
5 df-cnv 5527 . . . . 5 ∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧}
6 df-opab 5093 . . . . 5 {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧} = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
75, 6eqtri 2821 . . . 4 ∅ = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
87abeq2i 2925 . . 3 (𝑥∅ ↔ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧))
94, 8mtbir 326 . 2 ¬ 𝑥
109nel0 4264 1 ∅ = ∅
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  ∅c0 4243  ⟨cop 4531   class class class wbr 5030  {copab 5092  ◡ccnv 5518 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-dif 3884  df-nul 4244  df-br 5031  df-opab 5093  df-cnv 5527 This theorem is referenced by:  xp0  5982  cnveq0  6021  co01  6081  funcnv0  6390  f1o00  6624  tpos0  7905  oduleval  17733  ust0  22825  nghmfval  23328  isnghm  23329  1pthdlem1  27920  tocycf  30809  tocyc01  30810  mthmval  32935  resnonrel  40290  cononrel1  40292  cononrel2  40293  cnvrcl0  40323  0cnf  42517
 Copyright terms: Public domain W3C validator