Definition df-eu 1877

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 1899, eu2 1918, eu3 1920, and eu5 1921 (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 1967). (Contributed by NM, 5-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 1874	. 2 wff ∃!xφ
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1366	. . . . 5 wff x = y
6	1, 5	wb 98	. . . 4 wff (φ ↔ x = y)
7	6, 2	wal 1222	. . 3 wff ∀x(φ ↔ x = y)
8	7, 4	wex 1355	. 2 wff ∃y∀x(φ ↔ x = y)
9	3, 8	wb 98	1 wff (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

This definition is referenced by:  euf  1879  eubidh  1880  eubid  1881  hbeu1  1884  nfeu1  1885  sb8eu  1887  nfeudv  1889  nfeuv  1892  sb8euh  1897  exists1  1970  reu6  2699  euabsn2  3403  euotd  3955  iotauni  4795  iota1  4797  iotanul  4798  euiotaex  4799  iota4  4801  fv3  5111  eufnfv  5303