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 1925, eu2 1944, eu3 1946, and eu5 1947 (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 1993). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-eu |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | 1, 2 | weu 1900 | . 2 |
4 | vy | . . . . . 6 | |
5 | 2, 4 | weq 1392 | . . . . 5 |
6 | 1, 5 | wb 98 | . . . 4 |
7 | 6, 2 | wal 1241 | . . 3 |
8 | 7, 4 | wex 1381 | . 2 |
9 | 3, 8 | wb 98 | 1 |
Colors of variables: wff set class |
This definition is referenced by: euf 1905 eubidh 1906 eubid 1907 hbeu1 1910 nfeu1 1911 sb8eu 1913 nfeudv 1915 nfeuv 1918 sb8euh 1923 exists1 1996 reu6 2730 euabsn2 3439 euotd 3991 iotauni 4879 iota1 4881 iotanul 4882 euiotaex 4883 iota4 4885 fv3 5197 eufnfv 5389 |
Copyright terms: Public domain | W3C validator |