![]() |
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 1960 |
. 2
![]() ![]() ![]() ![]() |
4 | vy |
. . . . . 6
![]() ![]() | |
5 | 2, 4 | weq 1447 |
. . . . 5
![]() ![]() ![]() ![]() |
6 | 1, 5 | wb 104 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6, 2 | wal 1297 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 4 | wex 1436 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 8 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: euf 1965 eubidh 1966 eubid 1967 hbeu1 1970 nfeu1 1971 sb8eu 1973 nfeudv 1975 nfeuv 1978 sb8euh 1983 exists1 2056 reu6 2826 euabsn2 3539 euotd 4114 iotauni 5036 iota1 5038 iotanul 5039 euiotaex 5040 iota4 5042 fv3 5376 eufnfv 5580 |
Copyright terms: Public domain | W3C validator |