Theorem eu4 2640

Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)

Hypothesis

Ref	Expression
eu4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
eu4	⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem eu4

Step	Hyp	Ref	Expression
1		df-eu 2594	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		eu4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	mo4 2591	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
4	3	anbi2i 635	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
5	1, 4	bitri 278	1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  ∃wex 1811  ∃*wmo 2562  ∃!weu 2593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564  df-eu 2594

This theorem is used by:  euind  3681  eqeuel  4312  uniintsn  4944  eusv1  5353  omeu  8601  eroveu  8841  climeu  15731  pceu  17033  initoeu2lem2  18199  psgneu  19729  gsumval3eu  20127  frgr3vlem2  30884  3vfriswmgrlem  30887  onvfowev  36001  unirep  38785  rlimdmafv  48383  rlimdmafv2  48464