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

Definition df-mo 2223
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 2258. For other possible definitions see mo2 2229 and mo4 2269. (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 2219 . 2  wff  E* x ph
41, 2wex 1620 . . 3  wff  E. x ph
51, 2weu 2218 . . 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  2225  mo2vOLD  2226  mo2vOLDOLD  2227  nfmo1  2231  nfmod2  2233  mobid  2239  exmo  2245  eu5  2246  moabs  2251  exmoeu  2252  sb8mo  2255  cbvmo  2257  2euex  2297  2eu1  2307  bm1.1  2365  rmo5  3001  moeq  3200  funeu  5520  dffun8  5523  modom  7637  climmo  13382  rmoxfrdOLD  27508  rmoxfrd  27509  mont  30027  amosym1  30044  wl-sb8mot  30188  moxfr  30790
  Copyright terms: Public domain W3C validator