Theorem moeu 2656

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

Assertion

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

Proof of Theorem moeu

Step	Hyp	Ref	Expression
1		moabs 2609	. 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
2		exmoeub 2653	. . 3 ⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
3	2	pm5.74i 263	. 2 ⊢ ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
4	1, 3	bitri 267	1 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 198  ∃wex 1878  ∃*wmo 2603  ∃!weu 2639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-mo 2605  df-eu 2640

This theorem is referenced by:  dfeu  2667  dfmo  2668  exmoOLD  2672  mobidvOLDOLD  2674  nfmo1OLD  2675  nfmod2OLD  2677  mobidOLDOLD  2681  dfeuOLD  2683  moabsOLD  2684  exmoeuOLD  2685  sb8mo  2689  cbvmoOLD  2693  2euex  2724  2eu1  2733  bm1.1OLD  2809  rmo5  3374  moeqOLD  3607  zfnuleuOLD  5012  funeu  6152  dffun8  6155  modom  8436  climmo  14672  rmoxfrd  29881  nmotru  32936  amosym1  32953  bj-moeub  33350  wl-sb8mot  33899  nexmo1  34560  moxfr  38094  funressneu  41973  funressndmafv2rn  42119