Definition df-eu 1009

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 1019, eu2 1023, eu3 1024, and eu5 1035 (which in some cases we show with a hypothesis ph -> A.yph in place of a distinct variable condition on y and ph). Double uniqueness is tricky: E!xE!yph does not mean "exactly one x and one y" (see 2eu4 1070).

Assertion

Ref	Expression
df-eu	|- (E!xph <-> E.yA.x(ph <-> x = y))

Distinct variable group(s):   x,y   ph,y

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3	1, 2	weu 1007	. 2 wff E!xph
4		vy	. . . . . 6 set y
5	2, 4	weq 797	. . . . 5 wff x = y
6	1, 5	wb 127	. . . 4 wff (ph <-> x = y)
7	6, 2	wal 672	. . 3 wff A.x(ph <-> x = y)
8	7, 4	wex 678	. 2 wff E.yA.x(ph <-> x = y)
9	3, 8	wb 127	1 wff (E!xph <-> E.yA.x(ph <-> x = y))

This definition is referenced by:  euf 1011  bieud 1012  hbeu1 1015  hbeu 1016  sb8eu 1017  exists1 1072  eusn 1913  fv3 2839  aceq1 3552  aceq5 3563

metamath.org