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

Definition df-mo 2161
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 2187. For other possible definitions see mo2 2185 and mo4 2189. (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 2157 . 2  wff  E* x ph
41, 2wex 1531 . . 3  wff  E. x ph
51, 2weu 2156 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 176 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2167  nfmod2  2169  sb8mo  2175  mo2  2185  mobid  2190  cbvmo  2193  exmoeu  2198  moabs  2200  exmo  2201  2euex  2228  rmo5  2769  moeq  2954  funeu  5294  dffun8  5297  modom  7079  climmo  12047  rmoxfrdOLD  23162  rmoxfrd  23163  mont  24920  amosym1  24937  isconcl6a  26206  isconcl6ab  26207  moxfr  26855
  Copyright terms: Public domain W3C validator