Definition df-eu 1421

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 1431, eu2 1435, eu3 1436, and eu5 1448 (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 1492).

Assertion

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

Distinct variable groups:   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 1419	. 2 wff E!xph
4	2	cv 991	. . . . . 6 class x
5		vy	. . . . . . 7 set y
6	5	cv 991	. . . . . 6 class y
7	4, 6	wceq 992	. . . . 5 wff x = y
8	1, 7	wb 144	. . . 4 wff (ph <-> x = y)
9	8, 2	wal 990	. . 3 wff A.x(ph <-> x = y)
10	9, 5	wex 1016	. 2 wff E.yA.x(ph <-> x = y)
11	3, 10	wb 144	1 wff (E!xph <-> E.yA.x(ph <-> x = y))

This definition is referenced by:  euf 1423  eubid 1424  hbeu1 1427  hbeu 1428  sb8eu 1429  exists1 1498  reu3 1977  eusn 2507  fv3 3844  aceq1 4875  aceq5 4886

Copyright terms: Public domain