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

Theorem euex 2656
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2674. (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 2634 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 ax6ev 2070 . . . . 5 𝑥 𝑥 = 𝑦
3 biimpr 211 . . . . . 6 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
43com12 32 . . . . 5 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑦) → 𝜑))
52, 4eximii 1921 . . . 4 𝑥((𝜑𝑥 = 𝑦) → 𝜑)
6519.35i 1968 . . 3 (∀𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
76exlimiv 2021 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
81, 7sylbi 208 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1635  wex 1859  ∃!weu 2630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-eu 2634
This theorem is referenced by:  eu5  2658  exmoeu  2665  euan  2694  eupickbi  2703  2eu2ex  2710  2exeu  2713  euxfr  3590  eusvnf  5061  eusvnfb  5062  reusv2lem2  5068  reusv2lem3  5069  csbiota  6090  dffv3  6400  tz6.12c  6429  ndmfv  6434  dff3  6590  csbriota  6843  eusvobj2  6863  fnoprabg  6987  zfrep6  7360  dfac5lem5  9229  initoeu1  16861  initoeu1w  16862  initoeu2  16866  termoeu1  16868  termoeu1w  16869  grpidval  17461  0g0  17464  txcn  21640  bnj605  31298  bnj607  31307  bnj906  31321  bnj908  31322  unnf  32721  unqsym1  32739  moxfr  37754  eu2ndop1stv  41711  afveu  41739  afv2eu  41824  tz6.12c-afv2  41828  dfatco  41842  zrninitoringc  42636
  Copyright terms: Public domain W3C validator