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

Definition df-mo 2274
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 2278 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 2270 . 2  wff  E* x ph
41, 2wex 1657 . . 3  wff  E. x ph
51, 2weu 2269 . . 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  2276  nfmo1  2280  nfmod2  2282  mobid  2288  exmo  2294  eu5  2295  moabs  2300  exmoeu  2301  sb8mo  2303  cbvmo  2305  2euex  2343  2eu1  2352  bm1.1  2406  rmo5  3046  moeq  3246  funeu  5625  dffun8  5628  modom  7782  climmo  13620  rmoxfrdOLD  28126  rmoxfrd  28127  mont  31074  amosym1  31091  wl-sb8mot  31871  moxfr  35503
  Copyright terms: Public domain W3C validator