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

Definition df-mo 2259
Description: Define "there exists at most one  x such that  ph." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2285. For other possible definitions see mo2 2283 and mo4 2287. (Contributed by NM, 8-Mar-1995.)
Assertion
Ref Expression
df-mo  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
31, 2wmo 2255 . 2  wff  E* x ph
41, 2wex 1547 . . 3  wff  E. x ph
51, 2weu 2254 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 177 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2265  nfmod2  2267  sb8mo  2273  mo2  2283  mobid  2288  cbvmo  2291  exmoeu  2296  moabs  2298  exmo  2299  2euex  2326  rmo5  2884  moeq  3070  funeu  5436  dffun8  5439  modom  7268  climmo  12306  rmoxfrdOLD  23932  rmoxfrd  23933  mont  26063  amosym1  26080  moxfr  26623
  Copyright terms: Public domain W3C validator