![]() |
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 x such that φ." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 1922, eu2 1941, eu3 1943, and eu5 1944 (which in some cases we show with a hypothesis φ → ∀yφ in place of a distinct variable condition on y and φ). Double uniqueness is tricky: ∃!x∃!yφ does not mean "exactly one x and one y " (see 2eu4 1990). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-eu | ⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff φ | |
2 | vx | . . 3 setvar x | |
3 | 1, 2 | weu 1897 | . 2 wff ∃!xφ |
4 | vy | . . . . . 6 setvar y | |
5 | 2, 4 | weq 1389 | . . . . 5 wff x = y |
6 | 1, 5 | wb 98 | . . . 4 wff (φ ↔ x = y) |
7 | 6, 2 | wal 1240 | . . 3 wff ∀x(φ ↔ x = y) |
8 | 7, 4 | wex 1378 | . 2 wff ∃y∀x(φ ↔ x = y) |
9 | 3, 8 | wb 98 | 1 wff (∃!xφ ↔ ∃y∀x(φ ↔ x = y)) |
Colors of variables: wff set class |
This definition is referenced by: euf 1902 eubidh 1903 eubid 1904 hbeu1 1907 nfeu1 1908 sb8eu 1910 nfeudv 1912 nfeuv 1915 sb8euh 1920 exists1 1993 reu6 2724 euabsn2 3430 euotd 3982 iotauni 4822 iota1 4824 iotanul 4825 euiotaex 4826 iota4 4828 fv3 5140 eufnfv 5332 |
Copyright terms: Public domain | W3C validator |