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 1995. For another possible definition see mo4 2002. (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 1942 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1421 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 1941 | . . 3 wff ∃!𝑥𝜑 |
6 | 4, 5 | wi 4 | . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑) |
7 | 3, 6 | wb 103 | 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: nfmo1 1953 sb8mo 1955 nfmod 1958 mon 1970 eumo 1973 mobidh 1975 mobid 1976 hbmo1 1979 hbmo 1980 cbvmo 1981 eu5 1988 moabs 1990 exmodc 1991 exmonim 1992 mo2r 1993 mo3h 1994 exmoeudc 2004 2euex 2028 rmo5 2569 moeq 2767 repizf2lem 3935 funeu 4946 dffun8 4949 climmo 10137 |
Copyright terms: Public domain | W3C validator |