Definition df-eu 1946

Description: Define existential uniqueness, i.e. "there exists exactly one x such that ph." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 1968, eu2 1987, eu3 1989, and eu5 1990 (which in some cases we show with a hypothesis ph -> A. y ph in place of a distinct variable condition on y and ph). Double uniqueness is tricky: E! x E! y ph does not mean "exactly one x and one y " (see 2eu4 2036). (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-eu	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )

Distinct variable groups:   x, y   ph, y

Allowed substitution hint:   ph( x)

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	weu 1943	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1433	. . . . 5 wff x = y
6	1, 5	wb 103	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1283	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1422	. 2 wff E. y A. x ( ph <-> x = y )
9	3, 8	wb 103	1 wff ( E! x ph <-> E. y A. x ( ph <-> x = y ) )

This definition is referenced by:  euf  1948  eubidh  1949  eubid  1950  hbeu1  1953  nfeu1  1954  sb8eu  1956  nfeudv  1958  nfeuv  1961  sb8euh  1966  exists1  2039  reu6  2792  euabsn2  3485  euotd  4044  iotauni  4944  iota1  4946  iotanul  4947  euiotaex  4948  iota4  4950  fv3  5271  eufnfv  5463