MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mo Unicode version

Definition df-mo 2318
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 2344. For other possible definitions see mo2 2340 and mo4 2363. (Contributed by NM, 8-Mar-1995.)
Assertion
Ref Expression
df-mo

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3
2 vx . . 3
31, 2wmo 2314 . 2
41, 2wex 1565 . . 3
51, 2weu 2313 . . 3
64, 5wi 4 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2322  nfmod2  2324  exmo  2333  moabs  2334  exmoeu  2336  exmoeuOLD  2337  mo2  2340  sb8mo  2343  mo2OLD  2360  mobid  2364  cbvmo  2367  2euex  2405  rmo5  2982  moeq  3173  funeu  5462  dffun8  5465  modom  7474  climmo  12882  rmoxfrdOLD  25004  rmoxfrd  25005  mont  27498  amosym1  27515  moxfr  28172
  Copyright terms: Public domain W3C validator