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 2053. For another possible definition see mo4 2060. (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 2000 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1468 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 1999 | . . 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 2011 sb8mo 2013 nfmod 2016 mon 2028 eumo 2031 mobidh 2033 mobid 2034 hbmo1 2037 hbmo 2038 cbvmo 2039 eu5 2046 moabs 2048 exmodc 2049 exmonim 2050 mo2r 2051 mo3h 2052 exmoeudc 2062 2euex 2086 rmo5 2646 moeq 2859 repizf2lem 4085 funeu 5148 dffun8 5151 climmo 11067 |
Copyright terms: Public domain | W3C validator |