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

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

Proof of Theorem moeu
StepHypRef Expression
1 moabs 2537 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
2 exmoeub 2574 . . 3 (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
32pm5.74i 270 . 2 ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
41, 3bitri 274 1 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wex 1781  ∃*wmo 2532  ∃!weu 2562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534  df-eu 2563
This theorem is referenced by:  dfeu  2589  dfmo  2590  sb8mo  2595  cbvmowOLD  2598  2euexv  2627  2euex  2637  2eu1  2646  2eu1v  2647  rmo5  3396  funeu  6570  dffun8  6573  modom  9240  climmo  15497  rmoxfrd  31720  nmotru  35281  bj-moeub  35716  wl-sb8mot  36431  nexmo1  37102  moeu2  37219  moxfr  41415  funressneu  45743  funressndmafv2rn  45917
  Copyright terms: Public domain W3C validator