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

Definition df-eu 1900
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 1922, eu2 1941, eu3 1943, and eu5 1944 (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 1990). (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 1897 . 2 wff ∃!xφ
4 vy . . . . . 6 setvar y
52, 4weq 1389 . . . . 5 wff x = y
61, 5wb 98 . . . 4 wff (φx = y)
76, 2wal 1240 . . 3 wff x(φx = y)
87, 4wex 1378 . 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  1902  eubidh  1903  eubid  1904  hbeu1  1907  nfeu1  1908  sb8eu  1910  nfeudv  1912  nfeuv  1915  sb8euh  1920  exists1  1993  reu6  2724  euabsn2  3430  euotd  3982  iotauni  4822  iota1  4824  iotanul  4825  euiotaex  4826  iota4  4828  fv3  5140  eufnfv  5332
  Copyright terms: Public domain W3C validator