![]() |
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 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.) |
Ref | Expression |
---|---|
df-eu | ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | weu 2026 | . 2 wff ∃!𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1503 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wb 105 | . . . 4 wff (𝜑 ↔ 𝑥 = 𝑦) |
7 | 6, 2 | wal 1351 | . . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
8 | 7, 4 | wex 1492 | . 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
9 | 3, 8 | wb 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 2709 reu6 2926 euabsn2 3661 euotd 4254 iotauni 5190 iota1 5192 iotanul 5193 euiotaex 5194 iota4 5196 eliotaeu 5205 fv3 5538 eufnfv 5747 |
Copyright terms: Public domain | W3C validator |