Theorem eu5 2496

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 836	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃!𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
2		euex 2494	. . 3 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
3	2	pm4.71ri 665	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃!𝑥𝜑))
4		df-mo 2475	. . 3 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
5	4	anbi2i 730	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
6	1, 3, 5	3bitr4i 292	1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∃wex 1704  ∃!weu 2470  ∃*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-eu 2474  df-mo 2475

This theorem is referenced by:  exmoeu2  2497  eu3v  2498  eumo  2499  eu2  2509  eu4  2518  euim  2523  2euex  2544  2euswap  2548  2exeu  2549  2eu4  2556  reu5  3159  reuss2  3907  n0moeu  3937  reusv2lem1  4868  funcnv3  5959  fnres  6007  mptfnf  6015  fnopabg  6017  brprcneu  6184  dff3  6372  finnisoeu  8936  dfac2  8953  recmulnq  9786  uptx  21428  hausflf2  21802  adjeu  28748  bnj151  30947  bnj600  30989  nosupno  31849  nosupfv  31852  bj-eu3f  32829  fzisoeu  39514  ellimciota  39846