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

Definition df-mo 2017
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 2067. For another possible definition see mo4 2074. (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 2014 . 2  wff  E* x ph
41, 2wex 1479 . . 3  wff  E. x ph
51, 2weu 2013 . . 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  2025  sb8mo  2027  nfmod  2030  mon  2042  eumo  2045  mobidh  2047  mobid  2048  hbmo1  2051  hbmo  2052  cbvmo  2053  eu5  2060  moabs  2062  exmodc  2063  exmonim  2064  mo2r  2065  mo3h  2066  exmoeudc  2076  2euex  2100  rmo5  2679  moeq  2897  repizf2lem  4135  funeu  5208  dffun8  5211  climmo  11226
  Copyright terms: Public domain W3C validator