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

Definition df-eu 1945
Description: Define existential uniqueness, i.e. "there exists exactly one 𝑥 such that 𝜑." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 1967, eu2 1986, eu3 1988, and eu5 1989 (which in some cases we show with a hypothesis 𝜑 → ∀𝑦𝜑 in place of a distinct variable condition on 𝑦 and 𝜑). Double uniqueness is tricky: ∃!𝑥∃!𝑦𝜑 does not mean "exactly one 𝑥 and one 𝑦 " (see 2eu4 2035). (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-eu (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2weu 1942 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1433 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 103 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1283 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1422 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 103 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff set class
This definition is referenced by:  euf  1947  eubidh  1948  eubid  1949  hbeu1  1952  nfeu1  1953  sb8eu  1955  nfeudv  1957  nfeuv  1960  sb8euh  1965  exists1  2038  reu6  2782  euabsn2  3463  euotd  4011  iotauni  4903  iota1  4905  iotanul  4906  euiotaex  4907  iota4  4909  fv3  5223  eufnfv  5415
  Copyright terms: Public domain W3C validator