Definition df-eu 2082

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 2104, eu2 2124, eu3 2126, and eu5 2127 (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 2173). (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 2079	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1552	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 105	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1396	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1541	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 105	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euf  2084  eubidh  2085  eubid  2086  hbeu1  2089  nfeu1  2090  sb8eu  2092  nfeudv  2094  nfeuv  2097  sb8euh  2102  exists1  2176  cbvreuvw  2774  reu6  2996  euabsn2  3744  euotd  4353  iotauni  5306  iota1  5308  iotanul  5309  euiotaex  5310  iota4  5313  eliotaeu  5322  fv3  5671  eufnfv  5895