Definition df-eu 2029

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 2051, eu2 2070, eu3 2072, and eu5 2073 (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 2119). (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 2026	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1503	. . . . 5 wff x = y
6	1, 5	wb 105	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1351	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1492	. 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  2031  eubidh  2032  eubid  2033  hbeu1  2036  nfeu1  2037  sb8eu  2039  nfeudv  2041  nfeuv  2044  sb8euh  2049  exists1  2122  cbvreuvw  2709  reu6  2926  euabsn2  3661  euotd  4252  iotauni  5187  iota1  5189  iotanul  5190  euiotaex  5191  iota4  5193  eliotaeu  5202  fv3  5535  eufnfv  5743