Definition df-eu 1944

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 1966, eu2 1985, eu3 1987, and eu5 1988 (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 2034). (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 1941	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1432	. . . . 5 wff x = y
6	1, 5	wb 103	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1282	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1421	. 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  1946  eubidh  1947  eubid  1948  hbeu1  1951  nfeu1  1952  sb8eu  1954  nfeudv  1956  nfeuv  1959  sb8euh  1964  exists1  2037  reu6  2781  euabsn2  3461  euotd  4009  iotauni  4899  iota1  4901  iotanul  4902  euiotaex  4903  iota4  4905  fv3  5218  eufnfv  5410