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

Definition df-mo 1882
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 1932. For another possible definition see mo4 1939. (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 1879 . 2 wff ∃*xφ
41, 2wex 1358 . . 3 wff xφ
51, 2weu 1878 . . 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  1890  sb8mo  1892  nfmod  1895  mon  1907  eumo  1910  mobidh  1912  mobid  1913  hbmo1  1916  hbmo  1917  cbvmo  1918  eu5  1925  moabs  1927  exmodc  1928  exmonim  1929  mo2r  1930  mo3h  1931  exmoeudc  1941  2euex  1965  rmo5  2499  moeq  2689  repizf2lem  3884  funeu  4848  dffun8  4851
  Copyright terms: Public domain W3C validator