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 497	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1780  ∃*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 207  df-an 396  df-eu 2564

This theorem is referenced by:  exmoeu  2576  dfeu  2590  euan  2616  euanv  2619  2exeuv  2627  eupickbi  2631  2eu2ex  2638  2exeu  2641  euxfrw  3675  euxfr  3677  eusvnf  5328  eusvnfb  5329  reusv2lem2  5335  reusv2lem3  5336  csbiota  6474  dffv3  6818  ndmfv  6854  dff3  7033  csbriota  7318  eusvobj2  7338  fnoprabg  7469  zfrep6  7887  dfac5lem5  10018  initoeu1  17918  initoeu1w  17919  initoeu2  17923  termoeu1  17925  termoeu1w  17926  grpidval  18569  0g0  18572  zrninitoringc  20591  txcn  23541  bnj605  34919  bnj607  34928  bnj906  34942  bnj908  34943  neufal  36450  unqsym1  36469  bj-moeub  36893  moxfr  42795  onexomgt  43344  onexoegt  43347  omabs2  43435  eu2ndop1stv  47235  afveu  47263  afv2eu  47348  tz6.12c-afv2  47352  dfatco  47366  initc  49202  thincn0eu  49542  termcterm2  49625  termc2  49629  eufunclem  49632  eufunc  49633  euendfunc  49637  arweuthinc  49640  arweutermc  49641  diag1f1o  49645  diag2f1o  49648  prstchom2ALT  49675