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 501 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1787  ∃*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 210  df-an 400  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  3634  euxfr  3636  eusvnf  5285  eusvnfb  5286  reusv2lem2  5292  reusv2lem3  5293  csbiota  6373  dffv3  6713  tz6.12c  6742  ndmfv  6747  dff3  6919  csbriota  7186  eusvobj2  7206  fnoprabg  7333  zfrep6  7728  dfac5lem5  9741  initoeu1  17517  initoeu1w  17518  initoeu2  17522  termoeu1  17524  termoeu1w  17525  grpidval  18133  0g0  18136  txcn  22523  bnj605  32600  bnj607  32609  bnj906  32623  bnj908  32624  neufal  34332  unqsym1  34351  bj-moeub  34770  moxfr  40217  eu2ndop1stv  44289  afveu  44317  afv2eu  44402  tz6.12c-afv2  44406  dfatco  44420  zrninitoringc  45302  thincn0eu  45986  prstchom2ALT  46031
  Copyright terms: Public domain W3C validator