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 2024, eu2 2043, eu3 2045, and eu5 2046 (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 2092). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-eu |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | 1, 2 | weu 1999 | . 2 |
4 | vy | . . . . . 6 | |
5 | 2, 4 | weq 1479 | . . . . 5 |
6 | 1, 5 | wb 104 | . . . 4 |
7 | 6, 2 | wal 1329 | . . 3 |
8 | 7, 4 | wex 1468 | . 2 |
9 | 3, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: euf 2004 eubidh 2005 eubid 2006 hbeu1 2009 nfeu1 2010 sb8eu 2012 nfeudv 2014 nfeuv 2017 sb8euh 2022 exists1 2095 reu6 2873 euabsn2 3592 euotd 4176 iotauni 5100 iota1 5102 iotanul 5103 euiotaex 5104 iota4 5106 fv3 5444 eufnfv 5648 |
Copyright terms: Public domain | W3C validator |