![]() |
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 2000 |
. 2
![]() ![]() ![]() ![]() |
4 | vy |
. . . . . 6
![]() ![]() | |
5 | 2, 4 | weq 1480 |
. . . . 5
![]() ![]() ![]() ![]() |
6 | 1, 5 | wb 104 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6, 2 | wal 1330 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 4 | wex 1469 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 8 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: euf 2005 eubidh 2006 eubid 2007 hbeu1 2010 nfeu1 2011 sb8eu 2013 nfeudv 2015 nfeuv 2018 sb8euh 2023 exists1 2096 reu6 2877 euabsn2 3600 euotd 4184 iotauni 5108 iota1 5110 iotanul 5111 euiotaex 5112 iota4 5114 fv3 5452 eufnfv 5656 |
Copyright terms: Public domain | W3C validator |