![]() |
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-eu |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | 1, 2 | weu 2038 |
. 2
![]() ![]() ![]() ![]() |
4 | vy |
. . . . . 6
![]() ![]() | |
5 | 2, 4 | weq 1514 |
. . . . 5
![]() ![]() ![]() ![]() |
6 | 1, 5 | wb 105 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6, 2 | wal 1362 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 4 | wex 1503 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 8 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: euf 2043 eubidh 2044 eubid 2045 hbeu1 2048 nfeu1 2049 sb8eu 2051 nfeudv 2053 nfeuv 2056 sb8euh 2061 exists1 2134 cbvreuvw 2724 reu6 2941 euabsn2 3676 euotd 4272 iotauni 5208 iota1 5210 iotanul 5211 euiotaex 5212 iota4 5215 eliotaeu 5224 fv3 5557 eufnfv 5767 |
Copyright terms: Public domain | W3C validator |