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

Definition df-eu 2029
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 2051, eu2 2070, eu3 2072, and eu5 2073 (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 2119). (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 2026 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1503 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 105 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1351 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1492 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 105 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff set class
This definition is referenced by:  euf  2031  eubidh  2032  eubid  2033  hbeu1  2036  nfeu1  2037  sb8eu  2039  nfeudv  2041  nfeuv  2044  sb8euh  2049  exists1  2122  cbvreuvw  2710  reu6  2927  euabsn2  3662  euotd  4255  iotauni  5191  iota1  5193  iotanul  5194  euiotaex  5195  iota4  5197  eliotaeu  5206  fv3  5539  eufnfv  5748
  Copyright terms: Public domain W3C validator