Theorem eu5 1988

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 1971	. . 3 |- ( E! x ph -> E. x ph )
2		eumo 1973	. . 3 |- ( E! x ph -> E* x ph )
3	1, 2	jca 300	. 2 |- ( E! x ph -> ( E. x ph /\ E* x ph ) )
4		df-mo 1945	. . . . 5 |- ( E* x ph <-> ( E. x ph -> E! x ph ) )
5	4	biimpi 118	. . . 4 |- ( E* x ph -> ( E. x ph -> E! x ph ) )
6	5	imp 122	. . 3 |- ( ( E* x ph /\ E. x ph ) -> E! x ph )
7	6	ancoms 264	. 2 |- ( ( E. x ph /\ E* x ph ) -> E! x ph )
8	3, 7	impbii 124	1 |- ( E! x ph <-> ( E. x ph /\ E* x ph ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   E.wex 1421   E!weu 1941   E*wmo 1942

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945

This theorem is referenced by:  exmoeu2  1989  euan  1997  eu4  2003  euim  2009  euexex  2026  2euex  2028  2euswapdc  2032  2exeu  2033  reu5  2566  reuss2  3244  funcnv3  4981  fnres  5035  fnopabg  5042  brprcneu  5191  dff3im  5333  recmulnqg  6581