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

Definition df-mo 1946
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 1996. For another possible definition see mo4 2003. (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 1943 . 2 wff ∃*𝑥𝜑
41, 2wex 1422 . . 3 wff 𝑥𝜑
51, 2weu 1942 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 103 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfmo1  1954  sb8mo  1956  nfmod  1959  mon  1971  eumo  1974  mobidh  1976  mobid  1977  hbmo1  1980  hbmo  1981  cbvmo  1982  eu5  1989  moabs  1991  exmodc  1992  exmonim  1993  mo2r  1994  mo3h  1995  exmoeudc  2005  2euex  2029  rmo5  2570  moeq  2768  repizf2lem  3943  funeu  4956  dffun8  4959  climmo  10275
  Copyright terms: Public domain W3C validator