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

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

Syntax hints:   → wi 4  ∃wex 1779  ∃*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 207  df-an 396  df-eu 2568

This theorem is referenced by:  exmoeu  2580  dfeu  2594  euan  2620  euanv  2623  2exeuv  2631  eupickbi  2635  2eu2ex  2642  2exeu  2645  euxfrw  3704  euxfr  3706  eusvnf  5362  eusvnfb  5363  reusv2lem2  5369  reusv2lem3  5370  csbiota  6523  dffv3  6871  tz6.12cOLD  6902  ndmfv  6910  dff3  7089  csbriota  7375  eusvobj2  7395  fnoprabg  7528  zfrep6  7951  dfac5lem5  10139  initoeu1  18022  initoeu1w  18023  initoeu2  18027  termoeu1  18029  termoeu1w  18030  grpidval  18637  0g0  18640  zrninitoringc  20634  txcn  23562  bnj605  34884  bnj607  34893  bnj906  34907  bnj908  34908  neufal  36370  unqsym1  36389  bj-moeub  36813  moxfr  42662  onexomgt  43212  onexoegt  43215  omabs2  43303  eu2ndop1stv  47102  afveu  47130  afv2eu  47215  tz6.12c-afv2  47219  dfatco  47233  thincn0eu  49265  termcterm2  49347  termc2  49351  eufunclem  49354  eufunc  49355  euendfunc  49359  arweuthinc  49362  arweutermc  49363  diag1f1o  49367  diag2f1o  49370  prstchom2ALT  49389