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

Definition df-eu 1948
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 1970, eu2 1989, eu3 1991, and eu5 1992 (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 2038). (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 1945 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1435 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 103 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1285 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1424 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 103 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff set class
This definition is referenced by:  euf  1950  eubidh  1951  eubid  1952  hbeu1  1955  nfeu1  1956  sb8eu  1958  nfeudv  1960  nfeuv  1963  sb8euh  1968  exists1  2041  reu6  2795  euabsn2  3496  euotd  4057  iotauni  4960  iota1  4962  iotanul  4963  euiotaex  4964  iota4  4966  fv3  5293  eufnfv  5488
  Copyright terms: Public domain W3C validator