Theorem euex 2624

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 2614	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2	1	simplbi 498	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1765  ∃*wmo 2576  ∃!weu 2613

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 2614

This theorem is referenced by:  exmoeu  2628  dfeu  2642  dfeuOLD  2649  exmoeuOLD  2651  euan  2676  euanv  2680  2exeuv  2689  eupickbi  2693  2eu2ex  2700  2exeu  2703  euxfr  3653  eusvnf  5191  eusvnfb  5192  reusv2lem2  5198  reusv2lem3  5199  csbiota  6225  dffv3  6541  tz6.12c  6570  ndmfv  6575  dff3  6736  csbriota  6996  eusvobj2  7016  fnoprabg  7138  zfrep6  7519  dfac5lem5  9406  initoeu1  17104  initoeu1w  17105  initoeu2  17109  termoeu1  17111  termoeu1w  17112  grpidval  17703  0g0  17706  txcn  21922  bnj605  31791  bnj607  31800  bnj906  31814  bnj908  31815  neufal  33365  unqsym1  33384  bj-moeub  33749  moxfr  38795  eu2ndop1stv  42862  afveu  42890  afv2eu  42975  tz6.12c-afv2  42979  dfatco  42993  zrninitoringc  43842