Theorem euex 2572

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

Syntax hints:   → wi 4  ∃wex 1782  ∃*wmo 2533  ∃!weu 2563

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 398  df-eu 2564

This theorem is referenced by:  exmoeu  2576  dfeu  2590  euan  2618  euanv  2621  2exeuv  2629  eupickbi  2633  2eu2ex  2640  2exeu  2643  euxfrw  3718  euxfr  3720  eusvnf  5391  eusvnfb  5392  reusv2lem2  5398  reusv2lem3  5399  csbiota  6537  dffv3  6888  tz6.12cOLD  6919  ndmfv  6927  dff3  7102  csbriota  7381  eusvobj2  7401  fnoprabg  7531  zfrep6  7941  dfac5lem5  10122  initoeu1  17961  initoeu1w  17962  initoeu2  17966  termoeu1  17968  termoeu1w  17969  grpidval  18580  0g0  18583  txcn  23130  bnj605  33918  bnj607  33927  bnj906  33941  bnj908  33942  neufal  35291  unqsym1  35310  bj-moeub  35728  moxfr  41430  onexomgt  41990  onexoegt  41993  omabs2  42082  eu2ndop1stv  45833  afveu  45861  afv2eu  45946  tz6.12c-afv2  45950  dfatco  45964  zrninitoringc  46969  thincn0eu  47652  prstchom2ALT  47699