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

Definition df-mo 1877
Description: Define "there exists at most one x such that φ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 1927. For another possible definition see mo4 1934. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-mo (∃*xφ ↔ (xφ∃!xφ))

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
31, 2wmo 1874 . 2 wff ∃*xφ
41, 2wex 1354 . . 3 wff xφ
51, 2weu 1873 . . 3 wff ∃!xφ
64, 5wi 4 . 2 wff (xφ∃!xφ)
73, 6wb 98 1 wff (∃*xφ ↔ (xφ∃!xφ))
Colors of variables: wff set class
This definition is referenced by:  nfmo1  1885  sb8mo  1887  nfmod  1890  mon  1902  eumo  1905  mobidh  1907  mobid  1908  hbmo1  1911  hbmo  1912  cbvmo  1913  eu5  1920  moabs  1922  exmodc  1923  exmonim  1924  mo2r  1925  mo3h  1926  exmoeudc  1936  2euex  1960  rmo5  2494  moeq  2684  repizf2lem  3877  funeu  4840  dffun8  4843
  Copyright terms: Public domain W3C validator