![]() |
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 1961 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wex 1436 |
. . 3
![]() ![]() ![]() ![]() |
5 | 1, 2 | weu 1960 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | wi 4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfmo1 1972 sb8mo 1974 nfmod 1977 mon 1989 eumo 1992 mobidh 1994 mobid 1995 hbmo1 1998 hbmo 1999 cbvmo 2000 eu5 2007 moabs 2009 exmodc 2010 exmonim 2011 mo2r 2012 mo3h 2013 exmoeudc 2023 2euex 2047 rmo5 2604 moeq 2812 repizf2lem 4025 funeu 5084 dffun8 5087 climmo 10906 |
Copyright terms: Public domain | W3C validator |