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 2495. For other possible definitions see mo2 2467 and mo4 2505. (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 2459 | . 2 wff ∃*𝑥𝜑 |
4 | 1, 2 | wex 1695 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | weu 2458 | . . 3 wff ∃!𝑥𝜑 |
6 | 4, 5 | wi 4 | . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑) |
7 | 3, 6 | wb 195 | 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: mo2v 2465 nfmo1 2469 nfmod2 2471 mobid 2477 exmo 2483 eu5 2484 moabs 2489 exmoeu 2490 sb8mo 2492 cbvmo 2494 2euex 2532 2eu1 2541 bm1.1 2595 rmo5 3139 moeq 3349 funeu 5828 dffun8 5831 modom 8046 climmo 14136 rmoxfrdOLD 28716 rmoxfrd 28717 mont 31578 amosym1 31595 wl-sb8mot 32539 moxfr 36273 |
Copyright terms: Public domain | W3C validator |