Theorem euex 2003

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

Syntax hints:   → wi 4   ∧ wa 103  ∀wal 1310  ∃wex 1449  [wsb 1716  ∃!weu 1973

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-eu 1976

This theorem is referenced by:  eu2  2017  eu3h  2018  eu5  2020  exmoeudc  2036  eupickbi  2055  2eu2ex  2062  euxfrdc  2837  repizf  4002  eusvnf  4332  eusvnfb  4333  tz6.12c  5403  ndmfvg  5404  nfvres  5406  0fv  5408  eusvobj2  5712  fnoprabg  5824  txcn  12279