Theorem eu5 2524

Description: Uniqueness in terms of "at most one." Revised to reduce dependencies on axioms. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.)

Assertion

Ref	Expression
eu5	⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Proof of Theorem eu5

Step	Hyp	Ref	Expression
1		abai 853	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃!𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
2		euex 2522	. . 3 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
3	2	pm4.71ri 666	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃!𝑥𝜑))
4		df-mo 2503	. . 3 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
5	4	anbi2i 730	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
6	1, 3, 5	3bitr4i 292	1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∃wex 1744  ∃!weu 2498  ∃*wmo 2499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-eu 2502  df-mo 2503

This theorem is referenced by:  exmoeu2  2525  eu3v  2526  eumoOLD  2528  eu2  2538  eu4  2547  euim  2552  2euex  2573  2euswap  2577  2exeu  2578  2eu4  2585  reu5  3189  reuss2  3940  n0moeu  3970  reusv2lem1  4898  funcnv3  5997  fnres  6045  mptfnf  6053  fnopabg  6055  brprcneu  6222  dff3  6412  finnisoeu  8974  dfac2  8991  recmulnq  9824  uptx  21476  hausflf2  21849  adjeu  28876  bnj151  31073  bnj600  31115  nosupno  31974  nosupfv  31977  bj-eu3f  32954  fzisoeu  39828  ellimciota  40164