New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-eu GIF version

Definition df-eu 2208
 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 2225, eu2 2229, eu3 2230, and eu5 2242 (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 2287). (Contributed by NM, 12-Aug-1993.)
Assertion
Ref Expression
df-eu (∃!xφyx(φx = y))
Distinct variable groups:   x,y   φ,y
Allowed substitution hint:   φ(x)

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
31, 2weu 2204 . 2 wff ∃!xφ
4 vy . . . . . 6 setvar y
52, 4weq 1643 . . . . 5 wff x = y
61, 5wb 176 . . . 4 wff (φx = y)
76, 2wal 1540 . . 3 wff x(φx = y)
87, 4wex 1541 . 2 wff yx(φx = y)
93, 8wb 176 1 wff (∃!xφyx(φx = y))
 Colors of variables: wff setvar class This definition is referenced by:  euf  2210  eubid  2211  nfeu1  2214  nfeud2  2216  sb8eu  2222  exists1  2293  reu6  3025  euabsn2  3791  dfeu2  4333  iotauni  4351  iota1  4353  iotanul  4354  iotaex  4356  iota4  4357  fv3  5341
 Copyright terms: Public domain W3C validator