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 2474
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 2506. For other possible definitions see mo2 2478 and mo4 2516. (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 2470 . 2 wff ∃*𝑥𝜑
41, 2wex 1701 . . 3 wff 𝑥𝜑
51, 2weu 2469 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 196 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  mo2v  2476  nfmo1  2480  nfmod2  2482  mobid  2488  exmo  2494  eu5  2495  moabs  2500  exmoeu  2501  sb8mo  2503  cbvmo  2505  2euex  2543  2eu1  2552  bm1.1  2606  rmo5  3155  moeq  3369  funeu  5882  dffun8  5885  modom  8121  climmo  14238  rmoxfrdOLD  29221  rmoxfrd  29222  mont  32103  amosym1  32120  wl-sb8mot  33031  moxfr  36774
  Copyright terms: Public domain W3C validator