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

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

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