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

Definition df-mo 1920
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 1970. For another possible definition see mo4 1977. (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 1917 . 2  wff  E* x ph
41, 2wex 1397 . . 3  wff  E. x ph
51, 2weu 1916 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 102 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfmo1  1928  sb8mo  1930  nfmod  1933  mon  1945  eumo  1948  mobidh  1950  mobid  1951  hbmo1  1954  hbmo  1955  cbvmo  1956  eu5  1963  moabs  1965  exmodc  1966  exmonim  1967  mo2r  1968  mo3h  1969  exmoeudc  1979  2euex  2003  rmo5  2542  moeq  2738  repizf2lem  3941  funeu  4953  dffun8  4956  climmo  10049
  Copyright terms: Public domain W3C validator