Definition df-eu 1881

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 1903, eu2 1922, eu3 1924, and eu5 1925 (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 1971). (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 1878	. 2 wff ∃!xφ
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1369	. . . . 5 wff x = y
6	1, 5	wb 98	. . . 4 wff (φ ↔ x = y)
7	6, 2	wal 1224	. . 3 wff ∀x(φ ↔ x = y)
8	7, 4	wex 1358	. 2 wff ∃y∀x(φ ↔ x = y)
9	3, 8	wb 98	1 wff (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

This definition is referenced by:  euf  1883  eubidh  1884  eubid  1885  hbeu1  1888  nfeu1  1889  sb8eu  1891  nfeudv  1893  nfeuv  1896  sb8euh  1901  exists1  1974  reu6  2703  euabsn2  3409  euotd  3961  iotauni  4802  iota1  4804  iotanul  4805  euiotaex  4806  iota4  4808  fv3  5118  eufnfv  5310