Definition df-eu 2048

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 2070, eu2 2089, eu3 2091, and eu5 2092 (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 2138). (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 2045	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1517	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 105	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1362	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1506	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 105	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euf  2050  eubidh  2051  eubid  2052  hbeu1  2055  nfeu1  2056  sb8eu  2058  nfeudv  2060  nfeuv  2063  sb8euh  2068  exists1  2141  cbvreuvw  2735  reu6  2953  euabsn2  3692  euotd  4288  iotauni  5232  iota1  5234  iotanul  5235  euiotaex  5236  iota4  5239  eliotaeu  5248  fv3  5584  eufnfv  5796