![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-mo | Structured version Visualization version 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 2637. For other possible definitions see mo2 2608 and mo4 2647. (Contributed by NM, 8-Mar-1995.) |
Ref | Expression |
---|---|
df-mo | ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | wmo 2600 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1845 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 2599 | . . 3 wff ∃!𝑥𝜑 |
6 | 4, 5 | wi 4 | . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑) |
7 | 3, 6 | wb 196 | 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: mo2v 2606 nfmo1 2610 nfmod2 2612 mobid 2618 exmo 2624 eu5 2625 eumo 2628 moabs 2631 exmoeu 2632 sb8mo 2634 cbvmo 2636 2euex 2674 2eu1 2683 bm1.1 2737 rmo5 3293 moeq 3515 funeu 6066 dffun8 6069 modom 8318 climmo 14479 rmoxfrdOLD 29632 rmoxfrd 29633 mont 32706 amosym1 32723 wl-sb8mot 33665 nexmo 34328 moxfr 37749 |
Copyright terms: Public domain | W3C validator |