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

Theorem euex 2492
 Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2509. (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 2472 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 ax6ev 1888 . . . . 5 𝑥 𝑥 = 𝑦
3 biimpr 210 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
43com12 32 . . . . 5 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑦) → 𝜑))
52, 4eximii 1762 . . . 4 𝑥((𝜑𝑥 = 𝑦) → 𝜑)
6519.35i 1804 . . 3 (∀𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
76exlimiv 1856 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
81, 7sylbi 207 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1479  ∃wex 1702  ∃!weu 2468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886 This theorem depends on definitions:  df-bi 197  df-ex 1703  df-eu 2472 This theorem is referenced by:  eu5  2494  exmoeu  2500  euan  2528  eupickbi  2537  2eu2ex  2544  2exeu  2547  euxfr  3386  eusvnf  4852  eusvnfb  4853  reusv2lem2  4860  reusv2lem2OLD  4861  reusv2lem3  4862  csbiota  5869  dffv3  6174  tz6.12c  6200  ndmfv  6205  dff3  6358  csbriota  6608  eusvobj2  6628  fnoprabg  6746  zfrep6  7119  dfac5lem5  8935  initoeu1  16642  initoeu1w  16643  initoeu2  16647  termoeu1  16649  termoeu1w  16650  grpidval  17241  0g0  17244  txcn  21410  bnj605  30951  bnj607  30960  bnj906  30974  bnj908  30975  unnf  32381  unqsym1  32399  moxfr  37074  eu2ndop1stv  40965  afveu  40996  zrninitoringc  41836
 Copyright terms: Public domain W3C validator