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

Definition df-mo 2150
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 2176. For other possible definitions see mo2 2174 and mo4 2178. (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 2146 . 2  wff  E* x ph
41, 2wex 1529 . . 3  wff  E. x ph
51, 2weu 2145 . . 3  wff  E! x ph
64, 5wi 6 . 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  2156  nfmod2  2158  sb8mo  2164  mo2  2174  mobid  2179  cbvmo  2182  exmoeu  2187  moabs  2189  exmo  2190  2euex  2217  rmo5  2758  moeq  2943  funeu  5245  dffun8  5248  modom  7059  climmo  12026  mont  24256  amosym1  24273  isconcl6a  25503  isconcl6ab  25504  moxfr  26152
  Copyright terms: Public domain W3C validator