![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-mo | Unicode version |
Description: Define "there exists
at most one ![]() ![]() |
Ref | Expression |
---|---|
df-mo |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | 1, 2 | wmo 2027 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wex 1492 |
. . 3
![]() ![]() ![]() ![]() |
5 | 1, 2 | weu 2026 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | wi 4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfmo1 2038 sb8mo 2040 nfmod 2043 mon 2055 eumo 2058 mobidh 2060 mobid 2061 hbmo1 2064 hbmo 2065 cbvmo 2066 eu5 2073 moabs 2075 exmodc 2076 exmonim 2077 mo2r 2078 mo3h 2079 exmoeudc 2089 2euex 2113 rmo5 2693 moeq 2913 repizf2lem 4162 funeu 5242 dffun8 5245 climmo 11306 |
Copyright terms: Public domain | W3C validator |