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

Theorem euex 2631
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2649. (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 2611 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 ax6ev 2056 . . . . 5 𝑥 𝑥 = 𝑦
3 biimpr 210 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
43com12 32 . . . . 5 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑦) → 𝜑))
52, 4eximii 1913 . . . 4 𝑥((𝜑𝑥 = 𝑦) → 𝜑)
6519.35i 1955 . . 3 (∀𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
76exlimiv 2007 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
81, 7sylbi 207 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1630  wex 1853  ∃!weu 2607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054
This theorem depends on definitions:  df-bi 197  df-ex 1854  df-eu 2611
This theorem is referenced by:  eu5  2633  exmoeu  2640  euan  2668  eupickbi  2677  2eu2ex  2684  2exeu  2687  euxfr  3533  eusvnf  5010  eusvnfb  5011  reusv2lem2  5018  reusv2lem2OLD  5019  reusv2lem3  5020  csbiota  6042  dffv3  6348  tz6.12c  6374  ndmfv  6379  dff3  6535  csbriota  6786  eusvobj2  6806  fnoprabg  6926  zfrep6  7299  dfac5lem5  9140  initoeu1  16862  initoeu1w  16863  initoeu2  16867  termoeu1  16869  termoeu1w  16870  grpidval  17461  0g0  17464  txcn  21631  bnj605  31284  bnj607  31293  bnj906  31307  bnj908  31308  unnf  32712  unqsym1  32730  moxfr  37757  eu2ndop1stv  41708  afveu  41739  zrninitoringc  42581
  Copyright terms: Public domain W3C validator