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

Definition df-mo 2288
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 2314. For other possible definitions see mo2 2312 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  set  x
31, 2wmo 2284 . 2  wff  E* x ph
41, 2wex 1551 . . 3  wff  E. x ph
51, 2weu 2283 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 178 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2294  nfmod2  2296  sb8mo  2302  mo2  2312  mobid  2317  cbvmo  2320  exmoeu  2325  moabs  2327  exmo  2328  2euex  2355  rmo5  2926  moeq  3112  funeu  5480  dffun8  5483  modom  7312  climmo  12356  rmoxfrdOLD  23984  rmoxfrd  23985  mont  26164  amosym1  26181  moxfr  26746
  Copyright terms: Public domain W3C validator