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

Definition df-mo 1981
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 2031. For another possible definition see mo4 2038. (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 1978 . 2  wff  E* x ph
41, 2wex 1453 . . 3  wff  E. x ph
51, 2weu 1977 . . 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  1989  sb8mo  1991  nfmod  1994  mon  2006  eumo  2009  mobidh  2011  mobid  2012  hbmo1  2015  hbmo  2016  cbvmo  2017  eu5  2024  moabs  2026  exmodc  2027  exmonim  2028  mo2r  2029  mo3h  2030  exmoeudc  2040  2euex  2064  rmo5  2623  moeq  2832  repizf2lem  4055  funeu  5118  dffun8  5121  climmo  11022
  Copyright terms: Public domain W3C validator