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

Definition df-mo 2287
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 2323. For other possible definitions see mo2 2293 and mo4 2337. (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 2283 . 2
41, 2wex 1612 . . 3
51, 2weu 2282 . . 3
64, 5wi 4 . 2
73, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  nfmo1  2295  nfmod2  2297  mobid  2303  exmo  2309  eu5  2310  moabs  2315  exmoeu  2316  sb8mo  2320  cbvmo  2322  mo2OLD  2334  2euex  2366  2eu1  2376  bm1.1  2440  rmo5  3076  moeq  3275  funeu  5617  dffun8  5620  modom  7740  climmo  13380  rmoxfrdOLD  27391  rmoxfrd  27392  mont  29874  amosym1  29891  wl-sb8mot  30023  moxfr  30624
  Copyright terms: Public domain W3C validator