![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-mo | GIF version |
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.) |
Ref | Expression |
---|---|
df-mo | ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | wmo 1974 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1449 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 1973 | . . 3 wff ∃!𝑥𝜑 |
6 | 4, 5 | wi 4 | . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑) |
7 | 3, 6 | wb 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 |