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 2031. For another possible definition see mo4 2038. (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 1978 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1453 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 1977 | . . 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 1989 sb8mo 1991 nfmod 1994 mon 2006 eumo 2009 mobidh 2011 mobid 2012 hbmo1 2015 hbmo 2016 cbvmo 2017 eu5 2024 moabs 2026 exmodc 2027 exmonim 2028 mo2r 2029 mo3h 2030 exmoeudc 2040 2euex 2064 rmo5 2623 moeq 2832 repizf2lem 4055 funeu 5118 dffun8 5121 climmo 11022 |
Copyright terms: Public domain | W3C validator |