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

Theorem euex 2637
 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 2629 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simplbi 501 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2596  ∃!weu 2628 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 210  df-an 400  df-eu 2629 This theorem is referenced by:  exmoeu  2641  dfeu  2656  euan  2683  euanv  2686  2exeuv  2694  eupickbi  2698  2eu2ex  2705  2exeu  2708  euxfrw  3660  euxfr  3662  eusvnf  5258  eusvnfb  5259  reusv2lem2  5265  reusv2lem3  5266  csbiota  6317  dffv3  6641  tz6.12c  6670  ndmfv  6675  dff3  6843  csbriota  7108  eusvobj2  7128  fnoprabg  7254  zfrep6  7640  dfac5lem5  9540  initoeu1  17265  initoeu1w  17266  initoeu2  17270  termoeu1  17272  termoeu1w  17273  grpidval  17865  0g0  17868  txcn  22238  bnj605  32301  bnj607  32310  bnj906  32324  bnj908  32325  neufal  33879  unqsym1  33898  bj-moeub  34304  moxfr  39648  eu2ndop1stv  43696  afveu  43724  afv2eu  43809  tz6.12c-afv2  43813  dfatco  43827  zrninitoringc  44710
 Copyright terms: Public domain W3C validator