![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-mo | Structured version Visualization version 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 2311 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wex 1674 |
. . 3
![]() ![]() ![]() ![]() |
5 | 1, 2 | weu 2310 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | wi 4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wb 189 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: mo2v 2317 nfmo1 2321 nfmod2 2323 mobid 2329 exmo 2335 eu5 2336 moabs 2341 exmoeu 2342 sb8mo 2344 cbvmo 2346 2euex 2384 2eu1 2393 bm1.1 2447 rmo5 3023 moeq 3226 funeu 5629 dffun8 5632 modom 7804 climmo 13676 rmoxfrdOLD 28184 rmoxfrd 28185 mont 31119 amosym1 31136 wl-sb8mot 31953 moxfr 35580 |
Copyright terms: Public domain | W3C validator |