Theorem euex 2580

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

Syntax hints:   → wi 4  ∃wex 1777  ∃*wmo 2541  ∃!weu 2571

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 207  df-an 396  df-eu 2572

This theorem is referenced by:  exmoeu  2584  dfeu  2598  euan  2624  euanv  2627  2exeuv  2635  eupickbi  2639  2eu2ex  2646  2exeu  2649  euxfrw  3743  euxfr  3745  eusvnf  5410  eusvnfb  5411  reusv2lem2  5417  reusv2lem3  5418  csbiota  6566  dffv3  6916  tz6.12cOLD  6947  ndmfv  6955  dff3  7134  csbriota  7420  eusvobj2  7440  fnoprabg  7573  zfrep6  7995  dfac5lem5  10196  initoeu1  18078  initoeu1w  18079  initoeu2  18083  termoeu1  18085  termoeu1w  18086  grpidval  18699  0g0  18702  zrninitoringc  20698  txcn  23655  bnj605  34883  bnj607  34892  bnj906  34906  bnj908  34907  neufal  36372  unqsym1  36391  bj-moeub  36815  moxfr  42648  onexomgt  43202  onexoegt  43205  omabs2  43294  eu2ndop1stv  47040  afveu  47068  afv2eu  47153  tz6.12c-afv2  47157  dfatco  47171  thincn0eu  48699  prstchom2ALT  48746