Theorem eu5 2101

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 2084	. . 3 |- ( E! x ph -> E. x ph )
2		eumo 2086	. . 3 |- ( E! x ph -> E* x ph )
3	1, 2	jca 306	. 2 |- ( E! x ph -> ( E. x ph /\ E* x ph ) )
4		df-mo 2058	. . . . 5 |- ( E* x ph <-> ( E. x ph -> E! x ph ) )
5	4	biimpi 120	. . . 4 |- ( E* x ph -> ( E. x ph -> E! x ph ) )
6	5	imp 124	. . 3 |- ( ( E* x ph /\ E. x ph ) -> E! x ph )
7	6	ancoms 268	. 2 |- ( ( E. x ph /\ E* x ph ) -> E! x ph )
8	3, 7	impbii 126	1 |- ( E! x ph <-> ( E. x ph /\ E* x ph ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   E.wex 1515   E!weu 2054   E*wmo 2055

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058

This theorem is referenced by:  exmoeu2  2102  euan  2110  eu4  2116  euim  2122  euexex  2139  2euex  2141  2euswapdc  2145  2exeu  2146  reu5  2723  reuss2  3453  funcnv3  5336  fnres  5392  fnopabg  5399  brprcneu  5569  dff3im  5725  recmulnqg  7504  uptx  14746