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 1778  ∃*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  3726  euxfr  3728  eusvnf  5391  eusvnfb  5392  reusv2lem2  5398  reusv2lem3  5399  csbiota  6553  dffv3  6901  tz6.12cOLD  6932  ndmfv  6940  dff3  7119  csbriota  7404  eusvobj2  7424  fnoprabg  7557  zfrep6  7980  dfac5lem5  10168  initoeu1  18057  initoeu1w  18058  initoeu2  18062  termoeu1  18064  termoeu1w  18065  grpidval  18675  0g0  18678  zrninitoringc  20677  txcn  23635  bnj605  34922  bnj607  34931  bnj906  34945  bnj908  34946  neufal  36408  unqsym1  36427  bj-moeub  36851  moxfr  42708  onexomgt  43258  onexoegt  43261  omabs2  43350  eu2ndop1stv  47142  afveu  47170  afv2eu  47255  tz6.12c-afv2  47259  dfatco  47273  thincn0eu  49105  termcterm2  49174  termc2  49176  eufunclem  49179  eufunc  49180  euendfunc  49184  arweuthinc  49187  arweutermc  49188  diag1f1o  49192  diag2f1o  49195  prstchom2ALT  49216