Definition df-eu 2461

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 2497, eu2 2496, eu3v 2485, and eu5 2483 (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 2543). (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 2457	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1860	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 194	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1472	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1694	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 194	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euequ1  2463  mo2v  2464  euf  2465  nfeu1  2467  nfeud2  2469  eubid  2475  euex  2481  sb8eu  2490  exists1  2548  reu6  3361  euabsn2  4203  euotd  4890  iotauni  5765  iota1  5767  iotanul  5768  iotaex  5770  iota4  5771  fv3  6100  eufnfv  6372  seqomlem2  7410  aceq1  8800  dfac5  8811  bnj89  29834  wl-eudf  32316  wl-euequ1f  32318  wl-sb8eut  32321  iotain  37423  iotaexeu  37424  iotasbc  37425  iotavalsb  37439  sbiota1  37440