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 2604
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 2637. For other possible definitions see mo2 2608 and mo4 2647. (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 2600 . 2 wff ∃*𝑥𝜑
41, 2wex 1845 . . 3 wff 𝑥𝜑
51, 2weu 2599 . . 3 wff ∃!𝑥𝜑
64, 5wi 4 . 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
73, 6wb 196 1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  mo2v  2606  nfmo1  2610  nfmod2  2612  mobid  2618  exmo  2624  eu5  2625  eumo  2628  moabs  2631  exmoeu  2632  sb8mo  2634  cbvmo  2636  2euex  2674  2eu1  2683  bm1.1  2737  rmo5  3293  moeq  3515  funeu  6066  dffun8  6069  modom  8318  climmo  14479  rmoxfrdOLD  29632  rmoxfrd  29633  mont  32706  amosym1  32723  wl-sb8mot  33665  nexmo  34328  moxfr  37749
  Copyright terms: Public domain W3C validator