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

Theorem cnv0 6159
Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5295, ax-nul 5305, ax-pr 5431. (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 5191 . . . . . 6 ¬ 𝑦𝑧
21intnan 486 . . . . 5 ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
32nex 1799 . . . 4 ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
43nex 1799 . . 3 ¬ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)
5 df-cnv 5692 . . . . 5 ∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧}
6 df-opab 5205 . . . . 5 {⟨𝑧, 𝑦⟩ ∣ 𝑦𝑧} = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
75, 6eqtri 2764 . . . 4 ∅ = {𝑥 ∣ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧)}
87eqabri 2884 . . 3 (𝑥∅ ↔ ∃𝑧𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦𝑧))
94, 8mtbir 323 . 2 ¬ 𝑥
109nel0 4353 1 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1539  wex 1778  wcel 2107  {cab 2713  c0 4332  cop 4631   class class class wbr 5142  {copab 5204  ccnv 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-12 2176  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-dif 3953  df-nul 4333  df-br 5143  df-opab 5205  df-cnv 5692
This theorem is referenced by:  xp0  6177  cnveq0  6216  co01  6280  funcnv0  6631  f1o00  6882  tpos0  8282  cnvfi  9217  oduleval  18335  ust0  24229  nghmfval  24744  isnghm  24745  1pthdlem1  30155  mptiffisupp  32703  tocycf  33138  tocyc01  33139  mthmval  35581  resnonrel  43610  cononrel1  43612  cononrel2  43613  cnvrcl0  43643  0cnf  45897
  Copyright terms: Public domain W3C validator