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

Theorem euex 2478
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2495. (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 2458 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 ax6ev 1876 . . . . 5 𝑥 𝑥 = 𝑦
3 biimpr 208 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
43com12 32 . . . . 5 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑦) → 𝜑))
52, 4eximii 1753 . . . 4 𝑥((𝜑𝑥 = 𝑦) → 𝜑)
6519.35i 1794 . . 3 (∀𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
76exlimiv 1844 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
81, 7sylbi 205 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472  wex 1694  ∃!weu 2454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874
This theorem depends on definitions:  df-bi 195  df-ex 1695  df-eu 2458
This theorem is referenced by:  eu5  2480  exmoeu  2486  euan  2514  eupickbi  2523  2eu2ex  2530  2exeu  2533  euxfr  3355  eusvnf  4779  eusvnfb  4780  reusv2lem2  4787  reusv2lem2OLD  4788  reusv2lem3  4789  csbiota  5780  dffv3  6081  tz6.12c  6105  ndmfv  6110  dff3  6262  csbriota  6498  eusvobj2  6517  fnoprabg  6634  zfrep6  7001  dfac5lem5  8807  initoeu1  16427  initoeu1w  16428  initoeu2  16432  termoeu1  16434  termoeu1w  16435  grpidval  17026  0g0  17029  txcn  21178  bnj605  30034  bnj607  30043  bnj906  30057  bnj908  30058  unnf  31379  unqsym1  31397  moxfr  36073  eu2ndop1stv  39652  afveu  39684  zrninitoringc  41862
  Copyright terms: Public domain W3C validator