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

Definition df-mo 2122
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 2147. For other possible definitions see mo2 2145 and mo4 2149. (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 2118 . 2  wff  E* x ph
41, 2wex 1537 . . 3  wff  E. x ph
51, 2weu 2117 . . 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  2128  nfmod2  2130  mo2  2145  mobid  2150  cbvmo  2153  exmoeu  2158  moabs  2160  exmo  2161  2euex  2188  rmo5  2726  moeq  2909  funeu  5203  dffun8  5206  modom  7017  climmo  11982  mont  24209  amosym1  24226  isconcl6a  25456  isconcl6ab  25457  moxfr  26105
  Copyright terms: Public domain W3C validator