Theorem moeu 2643

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 2598 was then proved as dfmo 2657. (Revised by BJ, 30-Sep-2022.)

Assertion

Ref	Expression
moeu	⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Proof of Theorem moeu

Step	Hyp	Ref	Expression
1		moabs 2601	. 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
2		exmoeub 2640	. . 3 ⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
3	2	pm5.74i 274	. 2 ⊢ ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
4	1, 3	bitri 278	1 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1781  ∃*wmo 2596  ∃!weu 2628

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 1911  ax-6 1970

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2598  df-eu 2629

This theorem is referenced by:  dfeu  2656  dfmo  2657  sb8mo  2662  cbvmowOLD  2664  2euexv  2693  2euex  2703  2eu1  2712  2eu1v  2713  rmo5  3379  funeu  6349  dffun8  6352  modom  8703  climmo  14906  rmoxfrd  30264  nmotru  33869  amosym1  33887  bj-moeub  34288  wl-sb8mot  34979  nexmo1  35668  moxfr  39633  funressneu  43639  funressndmafv2rn  43779