Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-mo | Unicode version |
Description: Define "there exists at most one such that ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2067. For another possible definition see mo4 2074. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-mo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | 1, 2 | wmo 2014 | . 2 |
4 | 1, 2 | wex 1479 | . . 3 |
5 | 1, 2 | weu 2013 | . . 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 2025 sb8mo 2027 nfmod 2030 mon 2042 eumo 2045 mobidh 2047 mobid 2048 hbmo1 2051 hbmo 2052 cbvmo 2053 eu5 2060 moabs 2062 exmodc 2063 exmonim 2064 mo2r 2065 mo3h 2066 exmoeudc 2076 2euex 2100 rmo5 2679 moeq 2897 repizf2lem 4135 funeu 5208 dffun8 5211 climmo 11226 |
Copyright terms: Public domain | W3C validator |