Theorem euex 2577

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

Syntax hints:   → wi 4  ∃wex 1779  ∃*wmo 2538  ∃!weu 2568

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 2569

This theorem is referenced by:  exmoeu  2581  dfeu  2595  euan  2621  euanv  2624  2exeuv  2632  eupickbi  2636  2eu2ex  2643  2exeu  2646  euxfrw  3709  euxfr  3711  eusvnf  5367  eusvnfb  5368  reusv2lem2  5374  reusv2lem3  5375  csbiota  6529  dffv3  6877  tz6.12cOLD  6908  ndmfv  6916  dff3  7095  csbriota  7382  eusvobj2  7402  fnoprabg  7535  zfrep6  7958  dfac5lem5  10146  initoeu1  18029  initoeu1w  18030  initoeu2  18034  termoeu1  18036  termoeu1w  18037  grpidval  18644  0g0  18647  zrninitoringc  20641  txcn  23569  bnj605  34943  bnj607  34952  bnj906  34966  bnj908  34967  neufal  36429  unqsym1  36448  bj-moeub  36872  moxfr  42690  onexomgt  43240  onexoegt  43243  omabs2  43331  eu2ndop1stv  47134  afveu  47162  afv2eu  47247  tz6.12c-afv2  47251  dfatco  47265  thincn0eu  49297  termcterm2  49379  termc2  49383  eufunclem  49386  eufunc  49387  euendfunc  49391  arweuthinc  49394  arweutermc  49395  diag1f1o  49399  diag2f1o  49402  prstchom2ALT  49421