![]() |
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 2090. For another possible definition see mo4 2097. (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 2037 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1502 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 2036 | . . 3 wff ∃!𝑥𝜑 |
6 | 4, 5 | wi 4 | . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑) |
7 | 3, 6 | wb 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 |