Definition df-eu 2603

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 2640, eu2 2639, eu3v 2627, and eu5 2625 (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 2686). (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 2599	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 2032	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 196	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1622	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1845	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 196	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euequ1  2605  mo2v  2606  euf  2607  nfeu1  2609  nfeud2  2611  eubid  2617  euex  2623  sb8eu  2633  exists1  2691  reu6  3528  euabsn2  4396  euotd  5115  iotauni  6016  iota1  6018  iotanul  6019  iotaex  6021  iota4  6022  fv3  6359  eufnfv  6646  seqomlem2  7707  aceq1  9122  dfac5  9133  bnj89  31088  wl-eudf  33659  wl-euequ1f  33661  wl-sb8eut  33664  iotain  39112  iotaexeu  39113  iotasbc  39114  iotavalsb  39128  sbiota1  39129