Definition df-eu 1375

Description: Define existential uniqueness, i.e. "there exists exactly one x such that φ." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 1385, eu2 1389, eu3 1390, and eu5 1402 (which in some cases we show with a hypothesis φ → ∀yφ in place of a distinct variable condition on y and φ). Double uniqueness is tricky: ∃!x∃!yφ does not mean "exactly one x and one y" (see 2eu4 1445).

Assertion

Ref	Expression
df-eu	⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

Distinct variable groups:   x,y   φ,y

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3	1, 2	weu 1373	. 2 wff ∃!xφ
4	2	cv 952	. . . . . 6 class x
5		vy	. . . . . . 7 set y
6	5	cv 952	. . . . . 6 class y
7	4, 6	wceq 953	. . . . 5 wff x = y
8	1, 7	wb 146	. . . 4 wff (φ ↔ x = y)
9	8, 2	wal 951	. . 3 wff ∀x(φ ↔ x = y)
10	9, 5	wex 977	. 2 wff ∃y∀x(φ ↔ x = y)
11	3, 10	wb 146	1 wff (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

This definition is referenced by:  euf 1377  eubid 1378  hbeu1 1381  hbeu 1382  sb8eu 1383  exists1 1450  reu3 1921  eusn 2436  fv3 3718  aceq1 4701  aceq5 4712

Copyright terms: Public domain