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

Theorem euex 2493
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2510. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.)
Assertion
Ref Expression
euex (∃!𝑥𝜑 → ∃𝑥𝜑)

Proof of Theorem euex
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-eu 2473 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 ax6ev 1887 . . . . 5 𝑥 𝑥 = 𝑦
3 biimpr 210 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
43com12 32 . . . . 5 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑦) → 𝜑))
52, 4eximii 1761 . . . 4 𝑥((𝜑𝑥 = 𝑦) → 𝜑)
6519.35i 1803 . . 3 (∀𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
76exlimiv 1855 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
81, 7sylbi 207 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478  wex 1701  ∃!weu 2469
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
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-eu 2473
This theorem is referenced by:  eu5  2495  exmoeu  2501  euan  2529  eupickbi  2538  2eu2ex  2545  2exeu  2548  euxfr  3379  eusvnf  4831  eusvnfb  4832  reusv2lem2  4839  reusv2lem2OLD  4840  reusv2lem3  4841  csbiota  5850  dffv3  6154  tz6.12c  6180  ndmfv  6185  dff3  6338  csbriota  6588  eusvobj2  6608  fnoprabg  6726  zfrep6  7096  dfac5lem5  8910  initoeu1  16601  initoeu1w  16602  initoeu2  16606  termoeu1  16608  termoeu1w  16609  grpidval  17200  0g0  17203  txcn  21369  bnj605  30738  bnj607  30747  bnj906  30761  bnj908  30762  unnf  32101  unqsym1  32119  moxfr  36774  eu2ndop1stv  40536  afveu  40567  zrninitoringc  41389
  Copyright terms: Public domain W3C validator