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

Definition df-mo 2040
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 2090. For another possible definition see mo4 2097. (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 2037 . 2 wff ∃*𝑥𝜑
41, 2wex 1502 . . 3 wff 𝑥𝜑
51, 2weu 2036 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 105 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfmo1  2048  sb8mo  2050  nfmod  2053  mon  2065  eumo  2068  mobidh  2070  mobid  2071  hbmo1  2074  hbmo  2075  cbvmo  2076  eu5  2083  moabs  2085  exmodc  2086  exmonim  2087  mo2r  2088  mo3h  2089  exmoeudc  2099  2euex  2123  rmo5  2703  moeq  2924  repizf2lem  4173  funeu  5253  dffun8  5256  climmo  11319
  Copyright terms: Public domain W3C validator