Theorem moeu 2581

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

Assertion

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

Proof of Theorem moeu

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

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1781  ∃*wmo 2536  ∃!weu 2566

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 2538  df-eu 2567

This theorem is referenced by:  dfeu  2593  dfmo  2594  sb8mo  2599  cbvmowOLD  2602  2euexv  2631  2euex  2641  2eu1  2650  2eu1v  2651  rmo5  3372  funeu  6524  dffun8  6527  modom  9185  climmo  15436  rmoxfrd  31319  nmotru  34869  bj-moeub  35304  wl-sb8mot  36022  nexmo1  36694  moeu2  36812  moxfr  40991  funressneu  45251  funressndmafv2rn  45425