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

Definition df-mo 2273
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 2309. For other possible definitions see mo2 2279 and mo4 2323. (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 2269 . 2  wff  E* x ph
41, 2wex 1599 . . 3  wff  E. x ph
51, 2weu 2268 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 184 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff setvar class
This definition is referenced by:  mo2v  2275  mo2vOLD  2276  mo2vOLDOLD  2277  nfmo1  2281  nfmod2  2283  mobid  2289  exmo  2295  eu5  2296  moabs  2301  exmoeu  2302  sb8mo  2306  cbvmo  2308  mo2OLD  2320  2euex  2352  2eu1  2362  bm1.1  2426  rmo5  3062  moeq  3261  funeu  5602  dffun8  5605  modom  7722  climmo  13362  rmoxfrdOLD  27369  rmoxfrd  27370  mont  29850  amosym1  29867  wl-sb8mot  29999  moxfr  30600
  Copyright terms: Public domain W3C validator