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

Definition df-mo 2119
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 2144. For other possible definitions see mo2 2142 and mo4 2146. (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 2115 . 2  wff  E* x ph
41, 2wex 1537 . . 3  wff  E. x ph
51, 2weu 2114 . . 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  2125  nfmod2  2127  mo2  2142  mobid  2147  cbvmo  2150  exmoeu  2155  moabs  2157  exmo  2158  2euex  2185  moeq  2878  funeu  5136  dffun8  5139  modom  6948  climmo  11908  mont  24022  amosym1  24039  isconcl6a  25269  isconcl6ab  25270  moxfr  25918
  Copyright terms: Public domain W3C validator