Definition df-eu 1900

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 1922, eu2 1941, eu3 1943, and eu5 1944 (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 1990). (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 1897	. 2 wff ∃!xφ
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1389	. . . . 5 wff x = y
6	1, 5	wb 98	. . . 4 wff (φ ↔ x = y)
7	6, 2	wal 1240	. . 3 wff ∀x(φ ↔ x = y)
8	7, 4	wex 1378	. 2 wff ∃y∀x(φ ↔ x = y)
9	3, 8	wb 98	1 wff (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

This definition is referenced by:  euf  1902  eubidh  1903  eubid  1904  hbeu1  1907  nfeu1  1908  sb8eu  1910  nfeudv  1912  nfeuv  1915  sb8euh  1920  exists1  1993  reu6  2724  euabsn2  3430  euotd  3982  iotauni  4822  iota1  4824  iotanul  4825  euiotaex  4826  iota4  4828  fv3  5140  eufnfv  5332