Theorem euex 2107

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

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1393  ∃wex 1538  [wsb 1808  ∃!weu 2077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-eu 2080

This theorem is referenced by:  eu2  2122  eu3h  2123  eu5  2125  exmoeudc  2141  eupickbi  2160  2eu2ex  2167  euxfrdc  2990  repizf  4203  eusvnf  4548  eusvnfb  4549  tz6.12c  5665  ndmfvg  5666  elfvm  5668  nfvres  5671  0fv  5673  eusvobj2  5999  fnoprabg  6117  0g0  13449  txcn  14989