Theorem euex 2494

Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2511. (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 2474	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		ax6ev 1890	. . . . 5 ⊢ ∃𝑥 𝑥 = 𝑦
3		biimpr 210	. . . . . 6 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
4	3	com12 32	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝜑 ↔ 𝑥 = 𝑦) → 𝜑))
5	2, 4	eximii 1764	. . . 4 ⊢ ∃𝑥((𝜑 ↔ 𝑥 = 𝑦) → 𝜑)
6	5	19.35i 1806	. . 3 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
7	6	exlimiv 1858	. 2 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
8	1, 7	sylbi 207	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481  ∃wex 1704  ∃!weu 2470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-eu 2474

This theorem is referenced by:  eu5  2496  exmoeu  2502  euan  2530  eupickbi  2539  2eu2ex  2546  2exeu  2549  euxfr  3392  eusvnf  4861  eusvnfb  4862  reusv2lem2  4869  reusv2lem2OLD  4870  reusv2lem3  4871  csbiota  5881  dffv3  6187  tz6.12c  6213  ndmfv  6218  dff3  6372  csbriota  6623  eusvobj2  6643  fnoprabg  6761  zfrep6  7134  dfac5lem5  8950  initoeu1  16661  initoeu1w  16662  initoeu2  16666  termoeu1  16668  termoeu1w  16669  grpidval  17260  0g0  17263  txcn  21429  bnj605  30977  bnj607  30986  bnj906  31000  bnj908  31001  unnf  32406  unqsym1  32424  moxfr  37255  eu2ndop1stv  41202  afveu  41233  zrninitoringc  42071