Definition df-eu 2002

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 2024, eu2 2043, eu3 2045, and eu5 2046 (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 2092). (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 1999	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1479	. . . . 5 wff x = y
6	1, 5	wb 104	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1329	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1468	. 2 wff E. y A. x ( ph <-> x = y )
9	3, 8	wb 104	1 wff ( E! x ph <-> E. y A. x ( ph <-> x = y ) )

This definition is referenced by:  euf  2004  eubidh  2005  eubid  2006  hbeu1  2009  nfeu1  2010  sb8eu  2012  nfeudv  2014  nfeuv  2017  sb8euh  2022  exists1  2095  reu6  2873  euabsn2  3592  euotd  4176  iotauni  5100  iota1  5102  iotanul  5103  euiotaex  5104  iota4  5106  fv3  5444  eufnfv  5648