Theorem euex 2116

Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Assertion

Ref	Expression
euex	⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Proof of Theorem euex

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-17 1579	. . 3 ⊢ (𝜑 → ∀𝑦𝜑)
2	1	eu1 2111	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)))
3		exsimpl 1670	. 2 ⊢ (∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)) → ∃𝑥𝜑)
4	2, 3	sylbi 121	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  ∀wal 1400  ∃wex 1545  [wsb 1815  ∃!weu 2086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-eu 2089

This theorem is used by:  eu2  2131  eu3h  2132  eu5  2134  exmoeudc  2150  eupickbi  2169  2eu2ex  2176  euxfrdc  3012  repizf  4247  eusvnf  4599  eusvnfb  4600  tz6.12c  5725  ndmfvg  5726  elfvm  5729  nfvres  5732  0fv  5734  eusvobj2  6071  fnoprabg  6189  0g0  13696  ringidval  14265  txcn  15376  alseuals  17165