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

Definition df-mo 1964
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 2014. For another possible definition see mo4 2021. (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 1961 . 2  wff  E* x ph
41, 2wex 1436 . . 3  wff  E. x ph
51, 2weu 1960 . . 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  1972  sb8mo  1974  nfmod  1977  mon  1989  eumo  1992  mobidh  1994  mobid  1995  hbmo1  1998  hbmo  1999  cbvmo  2000  eu5  2007  moabs  2009  exmodc  2010  exmonim  2011  mo2r  2012  mo3h  2013  exmoeudc  2023  2euex  2047  rmo5  2604  moeq  2812  repizf2lem  4025  funeu  5084  dffun8  5087  climmo  10906
  Copyright terms: Public domain W3C validator