Definition df-eu 1009

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 1019, eu2 1023, eu3 1024, and eu5 1035 (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 1070).

Assertion

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

Distinct variable group(s):   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 1007	. 2 wff ∃!xφ
4		vy	. . . . . 6 set y
5	2, 4	weq 797	. . . . 5 wff x = y
6	1, 5	wb 127	. . . 4 wff (φ ↔ x = y)
7	6, 2	wal 672	. . 3 wff ∀x(φ ↔ x = y)
8	7, 4	wex 678	. 2 wff ∃y∀x(φ ↔ x = y)
9	3, 8	wb 127	1 wff (∃!xφ ↔ ∃y∀x(φ ↔ 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