Definition df-eu 2473

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 2509, eu2 2508, eu3v 2497, and eu5 2495 (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 2555). (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 2469	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1871	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 196	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1478	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1701	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 196	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euequ1  2475  mo2v  2476  euf  2477  nfeu1  2479  nfeud2  2481  eubid  2487  euex  2493  sb8eu  2502  exists1  2560  reu6  3382  euabsn2  4237  euotd  4945  iotauni  5832  iota1  5834  iotanul  5835  iotaex  5837  iota4  5838  fv3  6173  eufnfv  6456  seqomlem2  7506  aceq1  8900  dfac5  8911  bnj89  30548  wl-eudf  33025  wl-euequ1f  33027  wl-sb8eut  33030  iotain  38139  iotaexeu  38140  iotasbc  38141  iotavalsb  38155  sbiota1  38156