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

Definition df-eu 1877
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 1899, eu2 1918, eu3 1920, and eu5 1921 (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 1967). (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 1874 . 2 wff ∃!xφ
4 vy . . . . . 6 setvar y
52, 4weq 1366 . . . . 5 wff x = y
61, 5wb 98 . . . 4 wff (φx = y)
76, 2wal 1222 . . 3 wff x(φx = y)
87, 4wex 1355 . 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  1879  eubidh  1880  eubid  1881  hbeu1  1884  nfeu1  1885  sb8eu  1887  nfeudv  1889  nfeuv  1892  sb8euh  1897  exists1  1970  reu6  2699  euabsn2  3403  euotd  3955  iotauni  4795  iota1  4797  iotanul  4798  euiotaex  4799  iota4  4801  fv3  5111  eufnfv  5303
  Copyright terms: Public domain W3C validator