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

Definition df-mo 1947
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 1997. For another possible definition see mo4 2004. (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 1944 . 2  wff  E* x ph
41, 2wex 1422 . . 3  wff  E. x ph
51, 2weu 1943 . . 3  wff  E! x ph
64, 5wi 4 . 2  wff  ( E. x ph  ->  E! x ph )
73, 6wb 103 1  wff  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfmo1  1955  sb8mo  1957  nfmod  1960  mon  1972  eumo  1975  mobidh  1977  mobid  1978  hbmo1  1981  hbmo  1982  cbvmo  1983  eu5  1990  moabs  1992  exmodc  1993  exmonim  1994  mo2r  1995  mo3h  1996  exmoeudc  2006  2euex  2030  rmo5  2575  moeq  2778  repizf2lem  3961  funeu  4991  dffun8  4994  climmo  10509
  Copyright terms: Public domain W3C validator