![]() |
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 1901 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wex 1381 |
. . 3
![]() ![]() ![]() ![]() |
5 | 1, 2 | weu 1900 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | wi 4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wb 98 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfmo1 1912 sb8mo 1914 nfmod 1917 mon 1929 eumo 1932 mobidh 1934 mobid 1935 hbmo1 1938 hbmo 1939 cbvmo 1940 eu5 1947 moabs 1949 exmodc 1950 exmonim 1951 mo2r 1952 mo3h 1953 exmoeudc 1963 2euex 1987 rmo5 2525 moeq 2716 repizf2lem 3914 funeu 4926 dffun8 4929 climmo 9819 |
Copyright terms: Public domain | W3C validator |