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

Definition df-mo 2285
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 2311. For other possible definitions see mo2 2309 and mo4 2313. (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 2281 . 2  wff  E* x ph
41, 2wex 1550 . . 3  wff  E. x ph
51, 2weu 2280 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 177 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2291  nfmod2  2293  sb8mo  2299  mo2  2309  mobid  2314  cbvmo  2317  exmoeu  2322  moabs  2324  exmo  2325  2euex  2352  rmo5  2916  moeq  3102  funeu  5469  dffun8  5472  modom  7301  climmo  12343  rmoxfrdOLD  23971  rmoxfrd  23972  mont  26151  amosym1  26168  moxfr  26714
  Copyright terms: Public domain W3C validator