![]() |
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 2536. For other possible definitions see mo2 2507 and mo4 2546. (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 2499 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1744 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 2498 | . . 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 2505 nfmo1 2509 nfmod2 2511 mobid 2517 exmo 2523 eu5 2524 eumo 2527 moabs 2530 exmoeu 2531 sb8mo 2533 cbvmo 2535 2euex 2573 2eu1 2582 bm1.1 2636 rmo5 3192 moeq 3415 funeu 5951 dffun8 5954 modom 8202 climmo 14332 rmoxfrdOLD 29459 rmoxfrd 29460 mont 32533 amosym1 32550 wl-sb8mot 33490 nexmo 34153 moxfr 37572 |
Copyright terms: Public domain | W3C validator |