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

Theorem euex 2576
Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.)
Assertion
Ref Expression
euex (∃!𝑥𝜑 → ∃𝑥𝜑)

Proof of Theorem euex
StepHypRef Expression
1 df-eu 2568 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simplbi 499 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782  ∃*wmo 2537  ∃!weu 2567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-eu 2568
This theorem is referenced by:  exmoeu  2580  dfeu  2594  euan  2622  euanv  2625  2exeuv  2633  eupickbi  2637  2eu2ex  2644  2exeu  2647  euxfrw  3684  euxfr  3686  eusvnf  5352  eusvnfb  5353  reusv2lem2  5359  reusv2lem3  5360  csbiota  6494  dffv3  6843  tz6.12cOLD  6874  ndmfv  6882  dff3  7055  csbriota  7334  eusvobj2  7354  fnoprabg  7484  zfrep6  7892  dfac5lem5  10070  initoeu1  17904  initoeu1w  17905  initoeu2  17909  termoeu1  17911  termoeu1w  17912  grpidval  18523  0g0  18526  txcn  22993  bnj605  33559  bnj607  33568  bnj906  33582  bnj908  33583  neufal  34907  unqsym1  34926  bj-moeub  35344  moxfr  41044  onexomgt  41604  onexoegt  41607  omabs2  41696  eu2ndop1stv  45431  afveu  45459  afv2eu  45544  tz6.12c-afv2  45548  dfatco  45562  zrninitoringc  46443  thincn0eu  47126  prstchom2ALT  47173
  Copyright terms: Public domain W3C validator