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

Theorem cnv0 6141
Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5300, ax-nul 5307, ax-pr 5428. (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 5198 . . . . . 6 ¬ 𝑦𝑧
21intnan 488 . . . . 5 ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
32nex 1803 . . . 4 ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
43nex 1803 . . 3 ¬ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
5 df-cnv 5685 . . . . 5 ∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧}
6 df-opab 5212 . . . . 5 {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧} = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
75, 6eqtri 2761 . . . 4 ∅ = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
87eqabri 2878 . . 3 (𝑥∅ ↔ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧))
94, 8mtbir 323 . 2 ¬ 𝑥
109nel0 4351 1 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wex 1782  wcel 2107  {cab 2710  c0 4323  cop 4635   class class class wbr 5149  {copab 5211  ccnv 5676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-dif 3952  df-nul 4324  df-br 5150  df-opab 5212  df-cnv 5685
This theorem is referenced by:  xp0  6158  cnveq0  6197  co01  6261  funcnv0  6615  f1o00  6869  tpos0  8241  cnvfi  9180  oduleval  18242  ust0  23724  nghmfval  24239  isnghm  24240  1pthdlem1  29388  mptiffisupp  31915  tocycf  32276  tocyc01  32277  mthmval  34566  resnonrel  42343  cononrel1  42345  cononrel2  42346  cnvrcl0  42376  0cnf  44593
  Copyright terms: Public domain W3C validator