Theorem euex 2662

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

Syntax hints:   → wi 4  ∃wex 1780  ∃*wmo 2620  ∃!weu 2653

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 399  df-eu 2654

This theorem is referenced by:  exmoeu  2666  dfeu  2681  euan  2706  euanv  2709  2exeuv  2717  eupickbi  2721  2eu2ex  2728  2exeu  2731  euxfrw  3714  euxfr  3716  eusvnf  5295  eusvnfb  5296  reusv2lem2  5302  reusv2lem3  5303  csbiota  6350  dffv3  6668  tz6.12c  6697  ndmfv  6702  dff3  6868  csbriota  7131  eusvobj2  7151  fnoprabg  7277  zfrep6  7658  dfac5lem5  9555  initoeu1  17273  initoeu1w  17274  initoeu2  17278  termoeu1  17280  termoeu1w  17281  grpidval  17873  0g0  17876  txcn  22236  bnj605  32181  bnj607  32190  bnj906  32204  bnj908  32205  neufal  33756  unqsym1  33775  bj-moeub  34175  moxfr  39296  eu2ndop1stv  43331  afveu  43359  afv2eu  43444  tz6.12c-afv2  43448  dfatco  43462  zrninitoringc  44349