Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-eu | GIF version |
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 2002, eu2 2021, eu3 2023, and eu5 2024 (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 2070). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-eu | ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | weu 1977 | . 2 wff ∃!𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1464 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wb 104 | . . . 4 wff (𝜑 ↔ 𝑥 = 𝑦) |
7 | 6, 2 | wal 1314 | . . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
8 | 7, 4 | wex 1453 | . 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
9 | 3, 8 | wb 104 | 1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff set class |
This definition is referenced by: euf 1982 eubidh 1983 eubid 1984 hbeu1 1987 nfeu1 1988 sb8eu 1990 nfeudv 1992 nfeuv 1995 sb8euh 2000 exists1 2073 reu6 2846 euabsn2 3562 euotd 4146 iotauni 5070 iota1 5072 iotanul 5073 euiotaex 5074 iota4 5076 fv3 5412 eufnfv 5616 |
Copyright terms: Public domain | W3C validator |