Definition df-eu 2502

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 2539, eu2 2538, eu3v 2526, and eu5 2524 (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 2585). (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 2498	. 2 wff ∃!𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1931	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wb 196	. . . 4 wff (𝜑 ↔ 𝑥 = 𝑦)
7	6, 2	wal 1521	. . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
8	7, 4	wex 1744	. 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
9	3, 8	wb 196	1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This definition is referenced by:  euequ1  2504  mo2v  2505  euf  2506  nfeu1  2508  nfeud2  2510  eubid  2516  euex  2522  sb8eu  2532  exists1  2590  reu6  3428  euabsn2  4292  euotd  5004  iotauni  5901  iota1  5903  iotanul  5904  iotaex  5906  iota4  5907  fv3  6244  eufnfv  6531  seqomlem2  7591  aceq1  8978  dfac5  8989  bnj89  30915  wl-eudf  33484  wl-euequ1f  33486  wl-sb8eut  33489  iotain  38935  iotaexeu  38936  iotasbc  38937  iotavalsb  38951  sbiota1  38952