Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-eu | Unicode 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 2044, eu2 2063, eu3 2065, and eu5 2066 (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 2112). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-eu |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | 1, 2 | weu 2019 | . 2 |
4 | vy | . . . . . 6 | |
5 | 2, 4 | weq 1496 | . . . . 5 |
6 | 1, 5 | wb 104 | . . . 4 |
7 | 6, 2 | wal 1346 | . . 3 |
8 | 7, 4 | wex 1485 | . 2 |
9 | 3, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: euf 2024 eubidh 2025 eubid 2026 hbeu1 2029 nfeu1 2030 sb8eu 2032 nfeudv 2034 nfeuv 2037 sb8euh 2042 exists1 2115 cbvreuvw 2702 reu6 2919 euabsn2 3650 euotd 4237 iotauni 5170 iota1 5172 iotanul 5173 euiotaex 5174 iota4 5176 eliotaeu 5185 fv3 5517 eufnfv 5724 |
Copyright terms: Public domain | W3C validator |