Theorem eu5 2484

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 832	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃!𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
2		euex 2482	. . 3 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
3	2	pm4.71ri 663	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃!𝑥𝜑))
4		df-mo 2463	. . 3 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
5	4	anbi2i 726	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
6	1, 3, 5	3bitr4i 291	1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∃wex 1695  ∃!weu 2458  ∃*wmo 2459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-eu 2462  df-mo 2463

This theorem is referenced by:  exmoeu2  2485  eu3v  2486  eumo  2487  eu2  2497  eu4  2506  euim  2511  2euex  2532  2euswap  2536  2exeu  2537  2eu4  2544  reu5  3136  reuss2  3866  n0moeu  3893  reusv2lem1  4794  funcnv3  5873  fnres  5921  mptfnf  5928  fnopabg  5930  brprcneu  6096  dff3  6280  finnisoeu  8819  dfac2  8836  recmulnq  9665  uptx  21238  hausflf2  21612  adjeu  28132  bnj151  30201  bnj600  30243  bj-eu3f  32017  fzisoeu  38455  ellimciota  38681