Definition df-eu 2208

Description: Define existential uniqueness, i.e. "there exists exactly one x such that φ." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2225, eu2 2229, eu3 2230, and eu5 2242 (which in some cases we show with a hypothesis φ → ∀yφ in place of a distinct variable condition on y and φ). Double uniqueness is tricky: ∃!x∃!yφ does not mean "exactly one x and one y " (see 2eu4 2287). (Contributed by NM, 12-Aug-1993.)

Assertion

Ref	Expression
df-eu	⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

Distinct variable groups:   x,y   φ,y

Allowed substitution hint:   φ(x)

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3	1, 2	weu 2204	. 2 wff ∃!xφ
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1643	. . . . 5 wff x = y
6	1, 5	wb 176	. . . 4 wff (φ ↔ x = y)
7	6, 2	wal 1540	. . 3 wff ∀x(φ ↔ x = y)
8	7, 4	wex 1541	. 2 wff ∃y∀x(φ ↔ x = y)
9	3, 8	wb 176	1 wff (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

This definition is referenced by:  euf  2210  eubid  2211  nfeu1  2214  nfeud2  2216  sb8eu  2222  exists1  2293  reu6  3026  euabsn2  3792  dfeu2  4334  iotauni  4352  iota1  4354  iotanul  4355  iotaex  4357  iota4  4358  fv3  5342