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

Definition df-mo 1977
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 2027. For another possible definition see mo4 2034. (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 1974 . 2 wff ∃*𝑥𝜑
41, 2wex 1449 . . 3 wff 𝑥𝜑
51, 2weu 1973 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 104 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfmo1  1985  sb8mo  1987  nfmod  1990  mon  2002  eumo  2005  mobidh  2007  mobid  2008  hbmo1  2011  hbmo  2012  cbvmo  2013  eu5  2020  moabs  2022  exmodc  2023  exmonim  2024  mo2r  2025  mo3h  2026  exmoeudc  2036  2euex  2060  rmo5  2618  moeq  2826  repizf2lem  4043  funeu  5104  dffun8  5107  climmo  10953
  Copyright terms: Public domain W3C validator