Theorem euex 2602

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  ∃*wmo 2562  ∃!weu 2593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2594

This theorem is used by:  exmoeu  2606  dfeu  2620  euan  2646  euanv  2649  2exeuv  2657  eupickbi  2661  2eu2ex  2668  2exeu  2671  euxfrw  3679  euxfr  3681  zfrep6  5244  eusvnf  5357  eusvnfb  5358  reusv2lem2  5364  reusv2lem3  5365  csbiota  6526  dffv3  6875  ndmfv  6911  dff3  7094  csbriota  7386  eusvobj2  7406  fnoprabg  7537  zfrep6OLD  7953  dfac5lem5  10133  initoeu1  18103  initoeu1w  18104  initoeu2  18108  termoeu1  18110  termoeu1w  18111  grpidval  18757  0g0  18760  zrninitoringc  20841  txcn  23855  bnj605  35419  bnj607  35428  bnj906  35442  bnj908  35443  neufal  37028  unqsym1  37047  bj-moeub  37595  moxfr  43540  onexomgt  44085  onexoegt  44088  omabs2  44176  eu2ndop1stv  48016  afveu  48044  afv2eu  48129  tz6.12c-afv2  48133  dfatco  48147  initc  50020  thincn0eu  50360  termcterm2  50443  termc2  50447  eufunclem  50450  eufunc  50451  euendfunc  50455  arweuthinc  50458  arweutermc  50459  diag1f1o  50463  diag2f1o  50466  prstchom2ALT  50493  alseuals  50756