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

Definition df-mo 1901
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 1951. For another possible definition see mo4 1958. (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 1898 . 2 wff ∃*xφ
41, 2wex 1378 . . 3 wff xφ
51, 2weu 1897 . . 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  1909  sb8mo  1911  nfmod  1914  mon  1926  eumo  1929  mobidh  1931  mobid  1932  hbmo1  1935  hbmo  1936  cbvmo  1937  eu5  1944  moabs  1946  exmodc  1947  exmonim  1948  mo2r  1949  mo3h  1950  exmoeudc  1960  2euex  1984  rmo5  2519  moeq  2710  repizf2lem  3905  funeu  4869  dffun8  4872
  Copyright terms: Public domain W3C validator