Definition df-eu 2016

Description: Define existential uniqueness, i.e. "there exists exactly one 𝑥 such that 𝜑." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2038, eu2 2057, eu3 2059, and eu5 2060 (which in some cases we show with a hypothesis 𝜑 → ∀𝑦𝜑 in place of a distinct variable condition on 𝑦 and 𝜑). Double uniqueness is tricky: ∃!𝑥∃!𝑦𝜑 does not mean "exactly one 𝑥 and one 𝑦 " (see 2eu4 2106). (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-eu	⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	weu 2013	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1490	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 104	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1340	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1479	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 104	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euf  2018  eubidh  2019  eubid  2020  hbeu1  2023  nfeu1  2024  sb8eu  2026  nfeudv  2028  nfeuv  2031  sb8euh  2036  exists1  2109  cbvreuvw  2695  reu6  2910  euabsn2  3639  euotd  4226  iotauni  5159  iota1  5161  iotanul  5162  euiotaex  5163  iota4  5165  fv3  5503  eufnfv  5709