![]() |
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 1898 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wex 1378 |
. . 3
![]() ![]() ![]() ![]() |
5 | 1, 2 | weu 1897 |
. . 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 1909 sb8mo 1911 nfmod 1914 mon 1926 eumo 1929 mobidh 1931 mobid 1932 hbmo1 1935 hbmo 1936 cbvmo 1937 eu5 1944 moabs 1946 exmodc 1947 exmonim 1948 mo2r 1949 mo3h 1950 exmoeudc 1960 2euex 1984 rmo5 2519 moeq 2710 repizf2lem 3905 funeu 4869 dffun8 4872 |
Copyright terms: Public domain | W3C validator |