Theorem eu4 2699

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 2654	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		eu4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	mo4 2650	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
4	3	anbi2i 624	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
5	1, 4	bitri 277	1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535  ∃wex 1780  ∃*wmo 2620  ∃!weu 2653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622  df-eu 2654

This theorem is referenced by:  euind  3715  eqeuel  4322  uniintsn  4913  eusv1  5292  omeu  8211  eroveu  8392  climeu  14912  pceu  16183  initoeu2lem2  17275  psgneu  18634  gsumval3eu  19024  frgr3vlem2  28053  3vfriswmgrlem  28056  unirep  35003  rlimdmafv  43396  rlimdmafv2  43477