Theorem euex 2044

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 1514	. . 3 ⊢ (𝜑 → ∀𝑦𝜑)
2	1	eu1 2039	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)))
3		exsimpl 1605	. 2 ⊢ (∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)) → ∃𝑥𝜑)
4	2, 3	sylbi 120	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1341  ∃wex 1480  [wsb 1750  ∃!weu 2014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-eu 2017

This theorem is referenced by:  eu2  2058  eu3h  2059  eu5  2061  exmoeudc  2077  eupickbi  2096  2eu2ex  2103  euxfrdc  2912  repizf  4098  eusvnf  4431  eusvnfb  4432  tz6.12c  5516  ndmfvg  5517  nfvres  5519  0fv  5521  eusvobj2  5828  fnoprabg  5943  0g0  12607  txcn  12915