Definition df-eu 2083

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 2105, eu2 2125, eu3 2127, and eu5 2128 (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 2174). (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 2080	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1552	. . . . 5 wff x = y
6	1, 5	wb 105	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1396	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1541	. 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  2085  eubidh  2086  eubid  2087  hbeu1  2090  nfeu1  2091  sb8eu  2093  nfeudv  2095  nfeuv  2098  sb8euh  2103  exists1  2177  cbvreuvw  2784  reu6  3006  euabsn2  3760  euotd  4371  iotauni  5325  iota1  5327  iotanul  5328  euiotaex  5329  iota4  5332  eliotaeu  5341  fv3  5693  eufnfv  5917