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

Definition df-mo 2275
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 2315. For other possible definitions see mo2 2282 and mo4 2334. (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 2271 . 2  wff  E* x ph
41, 2wex 1591 . . 3  wff  E. x ph
51, 2weu 2270 . . 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  2277  mo2vOLD  2278  mo2vOLDOLD  2279  nfmo1  2284  nfmod2  2286  mobid  2292  exmo  2299  eu5  2300  moabs  2305  exmoeu  2306  exmoeuOLD  2307  sb8mo  2312  cbvmo  2314  mo2OLD  2331  2euex  2370  2eu1  2381  bm1.1  2445  rmo5  3075  moeq  3274  funeu  5605  dffun8  5608  modom  7712  climmo  13331  rmoxfrdOLD  27055  rmoxfrd  27056  mont  29439  amosym1  29456  wl-sb8mot  29588  moxfr  30217
  Copyright terms: Public domain W3C validator