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

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

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wmo 1946 . 2 wff ∃*𝑥𝜑
41, 2wex 1424 . . 3 wff 𝑥𝜑
51, 2weu 1945 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 103 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfmo1  1957  sb8mo  1959  nfmod  1962  mon  1974  eumo  1977  mobidh  1979  mobid  1980  hbmo1  1983  hbmo  1984  cbvmo  1985  eu5  1992  moabs  1994  exmodc  1995  exmonim  1996  mo2r  1997  mo3h  1998  exmoeudc  2008  2euex  2032  rmo5  2578  moeq  2781  repizf2lem  3973  funeu  5007  dffun8  5010  climmo  10584
  Copyright terms: Public domain W3C validator