ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-mo Unicode version

Definition df-mo 2003
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 2053. For another possible definition see mo4 2060. (Contributed by NM, 5-Aug-1993.)
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  setvar  x
31, 2wmo 2000 . 2  wff  E* x ph
41, 2wex 1468 . . 3  wff  E. x ph
51, 2weu 1999 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 104 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2011  sb8mo  2013  nfmod  2016  mon  2028  eumo  2031  mobidh  2033  mobid  2034  hbmo1  2037  hbmo  2038  cbvmo  2039  eu5  2046  moabs  2048  exmodc  2049  exmonim  2050  mo2r  2051  mo3h  2052  exmoeudc  2062  2euex  2086  rmo5  2646  moeq  2859  repizf2lem  4085  funeu  5148  dffun8  5151  climmo  11079
  Copyright terms: Public domain W3C validator