Definition df-eu 2029

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 2051, eu2 2070, eu3 2072, and eu5 2073 (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 2119). (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 2026	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1503	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 105	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1351	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1492	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 105	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euf  2031  eubidh  2032  eubid  2033  hbeu1  2036  nfeu1  2037  sb8eu  2039  nfeudv  2041  nfeuv  2044  sb8euh  2049  exists1  2122  cbvreuvw  2709  reu6  2926  euabsn2  3661  euotd  4253  iotauni  5189  iota1  5191  iotanul  5192  euiotaex  5193  iota4  5195  eliotaeu  5204  fv3  5537  eufnfv  5745