Definition df-eu 2474

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 2510, eu2 2509, eu3v 2498, and eu5 2496 (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 2556). (Contributed by NM, 12-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 2470	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1874	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 196	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1481	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1704	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 196	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euequ1  2476  mo2v  2477  euf  2478  nfeu1  2480  nfeud2  2482  eubid  2488  euex  2494  sb8eu  2503  exists1  2561  reu6  3395  euabsn2  4260  euotd  4975  iotauni  5863  iota1  5865  iotanul  5866  iotaex  5868  iota4  5869  fv3  6206  eufnfv  6491  seqomlem2  7546  aceq1  8940  dfac5  8951  bnj89  30787  wl-eudf  33354  wl-euequ1f  33356  wl-sb8eut  33359  iotain  38618  iotaexeu  38619  iotasbc  38620  iotavalsb  38634  sbiota1  38635