MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mo Structured version   Visualization version   GIF version

Definition df-mo 2635
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 2670. For other possible definitions see mo2 2641 and mo4 2680. (Contributed by NM, 8-Mar-1995.)
Assertion
Ref Expression
df-mo (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wmo 2631 . 2 wff ∃*𝑥𝜑
41, 2wex 1859 . . 3 wff 𝑥𝜑
51, 2weu 2630 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 197 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  mobidv  2637  mo2v  2639  nfmo1  2643  nfmod2  2645  mobid  2651  exmo  2657  eu5  2658  eumo  2661  moabs  2664  exmoeu  2665  sb8mo  2667  cbvmo  2669  2euex  2708  2eu1  2717  bm1.1OLD  2790  rmo5  3351  moeqOLD  3580  zfnuleuOLD  4980  funeu  6122  dffun8  6125  modom  8396  climmo  14507  rmoxfrdOLD  29654  rmoxfrd  29655  mont  32720  amosym1  32737  wl-sb8mot  33669  nexmo  34325  moxfr  37751  funressneu  41660  funressndmafv2rn  41806
  Copyright terms: Public domain W3C validator