Theorem eu5 2066

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	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )

Proof of Theorem eu5

Step	Hyp	Ref	Expression
1		euex 2049	. . 3 |- ( E! x ph -> E. x ph )
2		eumo 2051	. . 3 |- ( E! x ph -> E* x ph )
3	1, 2	jca 304	. 2 |- ( E! x ph -> ( E. x ph /\ E* x ph ) )
4		df-mo 2023	. . . . 5 |- ( E* x ph <-> ( E. x ph -> E! x ph ) )
5	4	biimpi 119	. . . 4 |- ( E* x ph -> ( E. x ph -> E! x ph ) )
6	5	imp 123	. . 3 |- ( ( E* x ph /\ E. x ph ) -> E! x ph )
7	6	ancoms 266	. 2 |- ( ( E. x ph /\ E* x ph ) -> E! x ph )
8	3, 7	impbii 125	1 |- ( E! x ph <-> ( E. x ph /\ E* x ph ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   E.wex 1485   E!weu 2019   E*wmo 2020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023

This theorem is referenced by:  exmoeu2  2067  euan  2075  eu4  2081  euim  2087  euexex  2104  2euex  2106  2euswapdc  2110  2exeu  2111  reu5  2682  reuss2  3407  funcnv3  5260  fnres  5314  fnopabg  5321  brprcneu  5489  dff3im  5641  recmulnqg  7353  uptx  13068