Definition df-eu 2022

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 2044, eu2 2063, eu3 2065, and eu5 2066 (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 2112). (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 2019	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1496	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 104	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1346	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1485	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 104	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euf  2024  eubidh  2025  eubid  2026  hbeu1  2029  nfeu1  2030  sb8eu  2032  nfeudv  2034  nfeuv  2037  sb8euh  2042  exists1  2115  cbvreuvw  2702  reu6  2919  euabsn2  3652  euotd  4239  iotauni  5172  iota1  5174  iotanul  5175  euiotaex  5176  iota4  5178  eliotaeu  5187  fv3  5519  eufnfv  5726