ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-eu Structured version   GIF version

Definition df-eu 1881
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 1903, eu2 1922, eu3 1924, and eu5 1925 (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 1971). (Contributed by NM, 5-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 1878 . 2 wff ∃!xφ
4 vy . . . . . 6 setvar y
52, 4weq 1369 . . . . 5 wff x = y
61, 5wb 98 . . . 4 wff (φx = y)
76, 2wal 1224 . . 3 wff x(φx = y)
87, 4wex 1358 . 2 wff yx(φx = y)
93, 8wb 98 1 wff (∃!xφyx(φx = y))
Colors of variables: wff set class
This definition is referenced by:  euf  1883  eubidh  1884  eubid  1885  hbeu1  1888  nfeu1  1889  sb8eu  1891  nfeudv  1893  nfeuv  1896  sb8euh  1901  exists1  1974  reu6  2703  euabsn2  3409  euotd  3961  iotauni  4802  iota1  4804  iotanul  4805  euiotaex  4806  iota4  4808  fv3  5118  eufnfv  5310
  Copyright terms: Public domain W3C validator