![]() |
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 1944 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wex 1422 |
. . 3
![]() ![]() ![]() ![]() |
5 | 1, 2 | weu 1943 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | wi 4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfmo1 1955 sb8mo 1957 nfmod 1960 mon 1972 eumo 1975 mobidh 1977 mobid 1978 hbmo1 1981 hbmo 1982 cbvmo 1983 eu5 1990 moabs 1992 exmodc 1993 exmonim 1994 mo2r 1995 mo3h 1996 exmoeudc 2006 2euex 2030 rmo5 2575 moeq 2778 repizf2lem 3961 funeu 4991 dffun8 4994 climmo 10509 |
Copyright terms: Public domain | W3C validator |