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

Definition df-eu 1903
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 1925, eu2 1944, eu3 1946, and eu5 1947 (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 1993). (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 1900 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1392 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 98 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1241 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1381 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 98 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff set class
This definition is referenced by:  euf  1905  eubidh  1906  eubid  1907  hbeu1  1910  nfeu1  1911  sb8eu  1913  nfeudv  1915  nfeuv  1918  sb8euh  1923  exists1  1996  reu6  2727  euabsn2  3436  euotd  3988  iotauni  4857  iota1  4859  iotanul  4860  euiotaex  4861  iota4  4863  fv3  5175  eufnfv  5367
  Copyright terms: Public domain W3C validator