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 2462
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 2494. For other possible definitions see mo2 2466 and mo4 2504. (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 2458 . 2 wff ∃*𝑥𝜑
41, 2wex 1694 . . 3 wff 𝑥𝜑
51, 2weu 2457 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 194 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  mo2v  2464  nfmo1  2468  nfmod2  2470  mobid  2476  exmo  2482  eu5  2483  moabs  2488  exmoeu  2489  sb8mo  2491  cbvmo  2493  2euex  2531  2eu1  2540  bm1.1  2594  rmo5  3138  moeq  3348  funeu  5813  dffun8  5816  modom  8023  climmo  14084  rmoxfrdOLD  28509  rmoxfrd  28510  mont  31371  amosym1  31388  wl-sb8mot  32322  moxfr  36056
  Copyright terms: Public domain W3C validator