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

Definition df-mo 2463
 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.)
Assertion
Ref Expression
df-mo (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wmo 2459 . 2 wff ∃*𝑥𝜑
41, 2wex 1695 . . 3 wff 𝑥𝜑
51, 2weu 2458 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 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