Theorem euex 2606

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

Syntax hints:   → wi 4  ∃wex 1801  ∃*wmo 2566  ∃!weu 2597

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 209  df-an 400  df-eu 2598

This theorem is referenced by:  exmoeu  2610  dfeu  2624  euan  2650  euanv  2653  2exeuv  2661  eupickbi  2665  2eu2ex  2672  2exeu  2675  euxfrw  3686  euxfr  3688  zfrep6  5241  eusvnf  5351  eusvnfb  5352  reusv2lem2  5358  reusv2lem3  5359  csbiota  6516  dffv3  6865  ndmfv  6901  dff3  7083  csbriota  7370  eusvobj2  7390  fnoprabg  7521  zfrep6OLD  7938  dfac5lem5  10085  initoeu1  18046  initoeu1w  18047  initoeu2  18051  termoeu1  18053  termoeu1w  18054  grpidval  18697  0g0  18700  zrninitoringc  20728  txcn  23688  bnj605  35204  bnj607  35213  bnj906  35227  bnj908  35228  neufal  36771  unqsym1  36790  bj-moeub  37339  moxfr  43278  onexomgt  43823  onexoegt  43826  omabs2  43914  eu2ndop1stv  47724  afveu  47752  afv2eu  47837  tz6.12c-afv2  47841  dfatco  47855  initc  49717  thincn0eu  50057  termcterm2  50140  termc2  50144  eufunclem  50147  eufunc  50148  euendfunc  50152  arweuthinc  50155  arweutermc  50156  diag1f1o  50160  diag2f1o  50163  prstchom2ALT  50190