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

Definition df-mo 2271
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 2306. For other possible definitions see mo2 2277 and mo4 2316. (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  setvar  x
31, 2wmo 2267 . 2  wff  E* x ph
41, 2wex 1659 . . 3  wff  E. x ph
51, 2weu 2266 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 187 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff setvar class
This definition is referenced by:  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  nfmo1  2279  nfmod2  2281  mobid  2287  exmo  2293  eu5  2294  moabs  2299  exmoeu  2300  sb8mo  2303  cbvmo  2305  2euex  2344  2eu1  2354  bm1.1  2412  rmo5  3054  moeq  3253  funeu  5625  dffun8  5628  modom  7779  climmo  13599  rmoxfrdOLD  27963  rmoxfrd  27964  mont  30854  amosym1  30871  wl-sb8mot  31610  moxfr  35242
  Copyright terms: Public domain W3C validator