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  3717  euxfr  3719  eusvnf  5390  eusvnfb  5391  reusv2lem2  5397  reusv2lem3  5398  csbiota  6534  dffv3  6885  tz6.12cOLD  6916  ndmfv  6924  dff3  7099  csbriota  7378  eusvobj2  7398  fnoprabg  7528  zfrep6  7938  dfac5lem5  10119  initoeu1  17958  initoeu1w  17959  initoeu2  17963  termoeu1  17965  termoeu1w  17966  grpidval  18577  0g0  18580  txcn  23122  bnj605  33907  bnj607  33916  bnj906  33930  bnj908  33931  neufal  35280  unqsym1  35299  bj-moeub  35717  moxfr  41416  onexomgt  41976  onexoegt  41979  omabs2  42068  eu2ndop1stv  45820  afveu  45848  afv2eu  45933  tz6.12c-afv2  45937  dfatco  45951  zrninitoringc  46923  thincn0eu  47606  prstchom2ALT  47653