Definition df-eu 2003

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 2025, eu2 2044, eu3 2046, and eu5 2047 (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 2093). (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 2000	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1480	. . . . 5 wff x = y
6	1, 5	wb 104	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1330	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1469	. 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  2005  eubidh  2006  eubid  2007  hbeu1  2010  nfeu1  2011  sb8eu  2013  nfeudv  2015  nfeuv  2018  sb8euh  2023  exists1  2096  reu6  2877  euabsn2  3600  euotd  4184  iotauni  5108  iota1  5110  iotanul  5111  euiotaex  5112  iota4  5114  fv3  5452  eufnfv  5656