Theorem euex 2581

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

Step	Hyp	Ref	Expression
1		df-eu 2573	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2	1	simplbi 497	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1786  ∃*wmo 2541  ∃!weu 2572

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 208  df-an 397  df-eu 2573

This theorem is referenced by:  exmoeu  2585  dfeu  2599  euan  2625  euanv  2628  2exeuv  2636  eupickbi  2640  2eu2ex  2647  2exeu  2650  euxfrw  3662  euxfr  3664  zfrep6  5212  eusvnf  5322  eusvnfb  5323  reusv2lem2  5329  reusv2lem3  5330  csbiota  6479  dffv3  6824  ndmfv  6860  dff3  7042  csbriota  7329  eusvobj2  7349  fnoprabg  7480  zfrep6OLD  7898  dfac5lem5  10041  initoeu1  17970  initoeu1w  17971  initoeu2  17975  termoeu1  17977  termoeu1w  17978  grpidval  18621  0g0  18624  zrninitoringc  20649  txcn  23610  bnj605  35098  bnj607  35107  bnj906  35121  bnj908  35122  neufal  36643  unqsym1  36662  bj-moeub  37211  moxfr  43150  onexomgt  43695  onexoegt  43698  omabs2  43786  eu2ndop1stv  47596  afveu  47624  afv2eu  47709  tz6.12c-afv2  47713  dfatco  47727  initc  49589  thincn0eu  49929  termcterm2  50012  termc2  50016  eufunclem  50019  eufunc  50020  euendfunc  50024  arweuthinc  50027  arweutermc  50028  diag1f1o  50032  diag2f1o  50035  prstchom2ALT  50062