Theorem eu5 2047

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 2030	. . 3 |- ( E! x ph -> E. x ph )
2		eumo 2032	. . 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 2004	. . . . 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 1469   E!weu 2000   E*wmo 2001

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004

This theorem is referenced by:  exmoeu2  2048  euan  2056  eu4  2062  euim  2068  euexex  2085  2euex  2087  2euswapdc  2091  2exeu  2092  reu5  2646  reuss2  3361  funcnv3  5193  fnres  5247  fnopabg  5254  brprcneu  5422  dff3im  5573  recmulnqg  7223  uptx  12482