Theorem euex 2482

Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2499. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.)

Assertion

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

Proof of Theorem euex

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-eu 2462	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		ax6ev 1877	. . . . 5 ⊢ ∃𝑥 𝑥 = 𝑦
3		biimpr 209	. . . . . 6 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
4	3	com12 32	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝜑 ↔ 𝑥 = 𝑦) → 𝜑))
5	2, 4	eximii 1754	. . . 4 ⊢ ∃𝑥((𝜑 ↔ 𝑥 = 𝑦) → 𝜑)
6	5	19.35i 1795	. . 3 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
7	6	exlimiv 1845	. 2 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
8	1, 7	sylbi 206	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  ∃wex 1695  ∃!weu 2458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-eu 2462

This theorem is referenced by:  eu5  2484  exmoeu  2490  euan  2518  eupickbi  2527  2eu2ex  2534  2exeu  2537  euxfr  3359  eusvnf  4787  eusvnfb  4788  reusv2lem2  4795  reusv2lem2OLD  4796  reusv2lem3  4797  csbiota  5797  dffv3  6099  tz6.12c  6123  ndmfv  6128  dff3  6280  csbriota  6523  eusvobj2  6542  fnoprabg  6659  zfrep6  7027  dfac5lem5  8833  initoeu1  16484  initoeu1w  16485  initoeu2  16489  termoeu1  16491  termoeu1w  16492  grpidval  17083  0g0  17086  txcn  21239  bnj605  30231  bnj607  30240  bnj906  30254  bnj908  30255  unnf  31576  unqsym1  31594  moxfr  36273  eu2ndop1stv  39851  afveu  39882  zrninitoringc  41863