![]() |
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 1967, eu2 1986, eu3 1988, and eu5 1989 (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 2035). (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 1942 | . 2 wff ∃!𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1433 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wb 103 | . . . 4 wff (𝜑 ↔ 𝑥 = 𝑦) |
7 | 6, 2 | wal 1283 | . . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
8 | 7, 4 | wex 1422 | . 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
9 | 3, 8 | wb 103 | 1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff set class |
This definition is referenced by: euf 1947 eubidh 1948 eubid 1949 hbeu1 1952 nfeu1 1953 sb8eu 1955 nfeudv 1957 nfeuv 1960 sb8euh 1965 exists1 2038 reu6 2782 euabsn2 3463 euotd 4011 iotauni 4903 iota1 4905 iotanul 4906 euiotaex 4907 iota4 4909 fv3 5223 eufnfv 5415 |
Copyright terms: Public domain | W3C validator |