Definition df-eu 2058

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 2080, eu2 2099, eu3 2101, and eu5 2102 (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 2148). (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 2055	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1527	. . . . 5 wff x = y
6	1, 5	wb 105	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1371	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1516	. 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  2060  eubidh  2061  eubid  2062  hbeu1  2065  nfeu1  2066  sb8eu  2068  nfeudv  2070  nfeuv  2073  sb8euh  2078  exists1  2151  cbvreuvw  2745  reu6  2964  euabsn2  3704  euotd  4304  iotauni  5250  iota1  5252  iotanul  5253  euiotaex  5254  iota4  5257  eliotaeu  5266  fv3  5609  eufnfv  5825