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

Theorem cnv0 5504
Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 4751, ax-nul 4759, ax-pr 4877. (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 4671 . . . . . 6 ¬ 𝑦𝑧
21intnan 959 . . . . 5 ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
32nex 1728 . . . 4 ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
43nex 1728 . . 3 ¬ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
5 df-cnv 5092 . . . . 5 ∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧}
6 df-opab 4684 . . . . 5 {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧} = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
75, 6eqtri 2643 . . . 4 ∅ = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
87abeq2i 2732 . . 3 (𝑥∅ ↔ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧))
94, 8mtbir 313 . 2 ¬ 𝑥
109nel0 3914 1 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1480  wex 1701  wcel 1987  {cab 2607  c0 3897  cop 4161   class class class wbr 4623  {copab 4682  ccnv 5083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-nul 3898  df-br 4624  df-opab 4684  df-cnv 5092
This theorem is referenced by:  xp0  5521  cnveq0  5560  co01  5619  funcnv0  5923  f10  6136  f1o00  6138  tpos0  7342  oduleval  17071  ust0  21963  nghmfval  22466  isnghm  22467  1pthdlem1  26895  mthmval  31233  resnonrel  37418  cononrel1  37420  cononrel2  37421  cnvrcl0  37452  0cnf  39425  mbf0  39510
  Copyright terms: Public domain W3C validator