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

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

Proof of Theorem moeu
StepHypRef Expression
1 moabs 2538 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
2 exmoeub 2575 . . 3 (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
32pm5.74i 271 . 2 ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
41, 3bitri 275 1 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wex 1782  ∃*wmo 2533  ∃!weu 2563
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 1914  ax-6 1972
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535  df-eu 2564
This theorem is referenced by:  dfeu  2590  dfmo  2591  sb8mo  2596  cbvmowOLD  2599  2euexv  2628  2euex  2638  2eu1  2647  2eu1v  2648  rmo5  3397  funeu  6574  dffun8  6577  modom  9244  climmo  15501  rmoxfrd  31733  nmotru  35293  bj-moeub  35728  wl-sb8mot  36443  nexmo1  37114  moeu2  37231  moxfr  41430  funressneu  45757  funressndmafv2rn  45931
  Copyright terms: Public domain W3C validator