Theorem euex 2603

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  ∃*wmo 2563  ∃!weu 2594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2595

This theorem is used by:  exmoeu  2607  dfeu  2621  euan  2647  euanv  2650  2exeuv  2658  eupickbi  2662  2eu2ex  2669  2exeu  2672  euxfrw  3679  euxfr  3681  zfrep6  5242  eusvnf  5354  eusvnfb  5355  reusv2lem2  5361  reusv2lem3  5362  csbiota  6531  dffv3  6881  ndmfv  6917  dff3  7100  csbriota  7392  eusvobj2  7412  fnoprabg  7543  zfrep6OLD  7967  dfac5lem5  10206  initoeu1  18186  initoeu1w  18187  initoeu2  18191  termoeu1  18193  termoeu1w  18194  grpidval  18840  0g0  18844  zrninitoringc  20928  txcn  23945  bnj605  35537  bnj607  35546  bnj906  35560  bnj908  35561  neufal  37194  unqsym1  37213  bj-moeub  37761  moxfr  43702  onexomgt  44242  onexoegt  44245  omabs2  44333  eu2ndop1stv  48194  afveu  48222  afv2eu  48307  tz6.12c-afv2  48311  dfatco  48325  initc  50198  thincn0eu  50538  termcterm2  50621  termc2  50625  eufunclem  50628  eufunc  50629  euendfunc  50633  arweuthinc  50636  arweutermc  50637  diag1f1o  50641  diag2f1o  50644  prstchom2ALT  50671  alseuals  50919