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

Theorem cnv0 5992
Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5194, ax-nul 5201, ax-pr 5320. (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 5106 . . . . . 6 ¬ 𝑦𝑧
21intnan 487 . . . . 5 ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
32nex 1792 . . . 4 ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
43nex 1792 . . 3 ¬ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
5 df-cnv 5556 . . . . 5 ∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧}
6 df-opab 5120 . . . . 5 {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧} = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
75, 6eqtri 2841 . . . 4 ∅ = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
87abeq2i 2945 . . 3 (𝑥∅ ↔ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧))
94, 8mtbir 324 . 2 ¬ 𝑥
109nel0 4308 1 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  wex 1771  wcel 2105  {cab 2796  c0 4288  cop 4563   class class class wbr 5057  {copab 5119  ccnv 5547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-dif 3936  df-nul 4289  df-br 5058  df-opab 5120  df-cnv 5556
This theorem is referenced by:  xp0  6008  cnveq0  6047  co01  6107  funcnv0  6413  f1o00  6642  tpos0  7911  oduleval  17729  ust0  22755  nghmfval  23258  isnghm  23259  1pthdlem1  27841  tocycf  30686  tocyc01  30687  mthmval  32719  resnonrel  39830  cononrel1  39832  cononrel2  39833  cnvrcl0  39863  0cnf  42036
  Copyright terms: Public domain W3C validator