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

Definition df-mo 2315
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 2347. For other possible definitions see mo2 2319 and mo4 2357. (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 2311 . 2  wff  E* x ph
41, 2wex 1674 . . 3  wff  E. x ph
51, 2weu 2310 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 189 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff setvar class
This definition is referenced by:  mo2v  2317  nfmo1  2321  nfmod2  2323  mobid  2329  exmo  2335  eu5  2336  moabs  2341  exmoeu  2342  sb8mo  2344  cbvmo  2346  2euex  2384  2eu1  2393  bm1.1  2447  rmo5  3023  moeq  3226  funeu  5629  dffun8  5632  modom  7804  climmo  13676  rmoxfrdOLD  28184  rmoxfrd  28185  mont  31119  amosym1  31136  wl-sb8mot  31953  moxfr  35580
  Copyright terms: Public domain W3C validator