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

Definition df-mo 2148
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 2174. For other possible definitions see mo2 2172 and mo4 2176. (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 2144 . 2  wff  E* x ph
41, 2wex 1528 . . 3  wff  E. x ph
51, 2weu 2143 . . 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  2154  nfmod2  2156  sb8mo  2162  mo2  2172  mobid  2177  cbvmo  2180  exmoeu  2185  moabs  2187  exmo  2188  2euex  2215  rmo5  2756  moeq  2941  funeu  5278  dffun8  5281  modom  7063  climmo  12031  rmoxfrdOLD  23146  rmoxfrd  23147  mont  24848  amosym1  24865  isconcl6a  26103  isconcl6ab  26104  moxfr  26752
  Copyright terms: Public domain W3C validator