Definition df-eu 2017

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 2039, eu2 2058, eu3 2060, and eu5 2061 (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 2107). (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 2014	. 2 wff E! x ph
4		vy	. . . . . 6 setvar y
5	2, 4	weq 1491	. . . . 5 wff x = y
6	1, 5	wb 104	. . . 4 wff ( ph <-> x = y )
7	6, 2	wal 1341	. . 3 wff A. x ( ph <-> x = y )
8	7, 4	wex 1480	. 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  2019  eubidh  2020  eubid  2021  hbeu1  2024  nfeu1  2025  sb8eu  2027  nfeudv  2029  nfeuv  2032  sb8euh  2037  exists1  2110  cbvreuvw  2697  reu6  2914  euabsn2  3644  euotd  4231  iotauni  5164  iota1  5166  iotanul  5167  euiotaex  5168  iota4  5170  fv3  5508  eufnfv  5714