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

Definition df-eu 2003
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 2025, eu2 2044, eu3 2046, and eu5 2047 (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 2093). (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 2000 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1480 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 104 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1330 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1469 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 104 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff set class
This definition is referenced by:  euf  2005  eubidh  2006  eubid  2007  hbeu1  2010  nfeu1  2011  sb8eu  2013  nfeudv  2015  nfeuv  2018  sb8euh  2023  exists1  2096  reu6  2874  euabsn2  3596  euotd  4180  iotauni  5104  iota1  5106  iotanul  5107  euiotaex  5108  iota4  5110  fv3  5448  eufnfv  5652
  Copyright terms: Public domain W3C validator