Definition df-eu 2080

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 2102, eu2 2122, eu3 2124, and eu5 2125 (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 2171). (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 2077	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1549	. . . . 5 wff x = y
6	1, 5	wb 105	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1393	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1538	. 2 wff E. y A. x ( ph <-> x = y )
9	3, 8	wb 105	1 wff ( E! x ph <-> E. y A. x ( ph <-> x = y ) )

This definition is referenced by:  euf  2082  eubidh  2083  eubid  2084  hbeu1  2087  nfeu1  2088  sb8eu  2090  nfeudv  2092  nfeuv  2095  sb8euh  2100  exists1  2174  cbvreuvw  2771  reu6  2992  euabsn2  3735  euotd  4340  iotauni  5287  iota1  5289  iotanul  5290  euiotaex  5291  iota4  5294  eliotaeu  5303  fv3  5646  eufnfv  5863