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

Theorem moeu 2662
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 2616 was then proved as dfmo 2676. (Revised by BJ, 30-Sep-2022.)
Assertion
Ref Expression
moeu (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Proof of Theorem moeu
StepHypRef Expression
1 moabs 2619 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
2 exmoeub 2659 . . 3 (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
32pm5.74i 273 . 2 ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
41, 3bitri 277 1 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wex 1774  ∃*wmo 2614  ∃!weu 2647
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-mo 2616  df-eu 2648
This theorem is referenced by:  dfeu  2675  dfmo  2676  sb8mo  2681  cbvmow  2682  2euexv  2710  2euex  2720  2eu1  2729  2eu1OLD  2730  2eu1v  2731  rmo5  3433  funeu  6373  dffun8  6376  modom  8711  climmo  14906  rmoxfrd  30249  nmotru  33749  amosym1  33767  bj-moeub  34166  wl-sb8mot  34806  nexmo1  35500  moxfr  39279  funressneu  43272  funressndmafv2rn  43412
  Copyright terms: Public domain W3C validator