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

Theorem moeu 2603
 Description: Uniqueness is equivalent to existence implying unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by NM, 8-Mar-1995.) This used to be the definition of the at-most-one quantifier, while df-mo 2558 was then proved as dfmo 2617. (Revised by BJ, 30-Sep-2022.)
Assertion
Ref Expression
moeu (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Proof of Theorem moeu
StepHypRef Expression
1 moabs 2561 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
2 exmoeub 2600 . . 3 (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
32pm5.74i 274 . 2 ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
41, 3bitri 278 1 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1782  ∃*wmo 2556  ∃!weu 2588 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-mo 2558  df-eu 2589 This theorem is referenced by:  dfeu  2616  dfmo  2617  sb8mo  2622  cbvmowOLD  2624  2euexv  2653  2euex  2663  2eu1  2672  2eu1v  2673  rmo5  3342  funeu  6353  dffun8  6356  modom  8733  climmo  14947  rmoxfrd  30348  nmotru  34131  amosym1  34149  bj-moeub  34554  wl-sb8mot  35244  nexmo1  35933  moxfr  39991  funressneu  43990  funressndmafv2rn  44132
 Copyright terms: Public domain W3C validator