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

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