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

Definition df-mo 2293
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 2319. For other possible definitions see mo2 2317 and mo4 2321. (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 2289 . 2
41, 2wex 1551 . . 3
51, 2weu 2288 . . 3
64, 5wi 4 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2299  nfmod2  2301  sb8mo  2307  mo2  2317  mobid  2322  cbvmo  2325  exmoeu  2330  moabs  2332  exmo  2333  2euex  2360  rmo5  2933  moeq  3119  funeu  5524  dffun8  5527  modom  7358  climmo  12402  rmoxfrdOLD  24028  rmoxfrd  24029  mont  26263  amosym1  26280  moxfr  26914
  Copyright terms: Public domain W3C validator