Theorem euex 2577

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

Syntax hints:   → wi 4  ∃wex 1783  ∃*wmo 2538  ∃!weu 2568

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 206  df-an 396  df-eu 2569

This theorem is referenced by:  exmoeu  2581  dfeu  2595  euan  2623  euanv  2626  2exeuv  2634  eupickbi  2638  2eu2ex  2645  2exeu  2648  euxfrw  3651  euxfr  3653  eusvnf  5310  eusvnfb  5311  reusv2lem2  5317  reusv2lem3  5318  csbiota  6411  dffv3  6752  tz6.12c  6781  ndmfv  6786  dff3  6958  csbriota  7228  eusvobj2  7248  fnoprabg  7375  zfrep6  7771  dfac5lem5  9814  initoeu1  17642  initoeu1w  17643  initoeu2  17647  termoeu1  17649  termoeu1w  17650  grpidval  18260  0g0  18263  txcn  22685  bnj605  32787  bnj607  32796  bnj906  32810  bnj908  32811  neufal  34522  unqsym1  34541  bj-moeub  34960  moxfr  40430  eu2ndop1stv  44504  afveu  44532  afv2eu  44617  tz6.12c-afv2  44621  dfatco  44635  zrninitoringc  45517  thincn0eu  46201  prstchom2ALT  46246