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

Definition df-mo 1904
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 1954. For another possible definition see mo4 1961. (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 1901 . 2 wff ∃*𝑥𝜑
41, 2wex 1381 . . 3 wff 𝑥𝜑
51, 2weu 1900 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 98 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfmo1  1912  sb8mo  1914  nfmod  1917  mon  1929  eumo  1932  mobidh  1934  mobid  1935  hbmo1  1938  hbmo  1939  cbvmo  1940  eu5  1947  moabs  1949  exmodc  1950  exmonim  1951  mo2r  1952  mo3h  1953  exmoeudc  1963  2euex  1987  rmo5  2525  moeq  2716  repizf2lem  3914  funeu  4926  dffun8  4929  climmo  9819
  Copyright terms: Public domain W3C validator