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

Definition df-mo 2310
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 2336. For other possible definitions see mo2 2332 and mo4 2355. (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 2306 . 2
41, 2wex 1557 . . 3
51, 2weu 2305 . . 3
64, 5wi 4 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2314  nfmod2  2316  exmo  2325  moabs  2326  exmoeu  2328  exmoeuOLD  2329  mo2  2332  sb8mo  2335  mo2OLD  2352  mobid  2356  cbvmo  2359  2euex  2397  rmo5  2973  moeq  3161  funeu  5441  dffun8  5444  modom  7421  climmo  12821  rmoxfrdOLD  24492  rmoxfrd  24493  mont  26989  amosym1  27006  moxfr  27664
  Copyright terms: Public domain W3C validator