Theorem eu5 2102

Description: Uniqueness in terms of "at most one". (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)

Assertion

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

Proof of Theorem eu5

Step	Hyp	Ref	Expression
1		euex 2085	. . 3 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
2		eumo 2087	. . 3 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)
3	1, 2	jca 306	. 2 ⊢ (∃!𝑥𝜑 → (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
4		df-mo 2059	. . . . 5 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
5	4	biimpi 120	. . . 4 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑))
6	5	imp 124	. . 3 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥𝜑) → ∃!𝑥𝜑)
7	6	ancoms 268	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) → ∃!𝑥𝜑)
8	3, 7	impbii 126	1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∃wex 1516  ∃!weu 2055  ∃*wmo 2056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059

This theorem is referenced by:  exmoeu2  2103  euan  2111  eu4  2117  euim  2123  euexex  2140  2euex  2142  2euswapdc  2146  2exeu  2147  reu5  2724  reuss2  3457  funcnv3  5345  fnres  5402  fnopabg  5409  brprcneu  5582  dff3im  5738  recmulnqg  7524  uptx  14821