Theorem eu5 1989

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 1972	. . 3 |- ( E! x ph -> E. x ph )
2		eumo 1974	. . 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 1946	. . . . 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 1422   E!weu 1942   E*wmo 1943

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 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946

This theorem is referenced by:  exmoeu2  1990  euan  1998  eu4  2004  euim  2010  euexex  2027  2euex  2029  2euswapdc  2033  2exeu  2034  reu5  2567  reuss2  3251  funcnv3  4992  fnres  5046  fnopabg  5053  brprcneu  5202  dff3im  5344  recmulnqg  6643