Theorem reu5 2703

Description: Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)

Assertion

Ref	Expression
reu5	|- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )

Proof of Theorem reu5

Step	Hyp	Ref	Expression
1		eu5 2085	. 2 |- ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
2		df-reu 2475	. 2 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		df-rex 2474	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4		df-rmo 2476	. . 3 |- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
5	3, 4	anbi12i 460	. 2 |- ( ( E. x e. A ph /\ E* x e. A ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
6	1, 2, 5	3bitr4i 212	1 |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )

Syntax hints:   /\ wa 104   <-> wb 105   E.wex 1503   E!weu 2038   E*wmo 2039   e. wcel 2160   E.wrex 2469   E!wreu 2470   E*wrmo 2471

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-rex 2474  df-reu 2475  df-rmo 2476

This theorem is referenced by:  reurex  2704  reurmo  2705  reu4  2946  reueq  2951  reusv1  4479  fncnv  5304  moriotass  5884  supeuti  7027  infeuti  7062  lteupri  7651  elrealeu  7863  rereceu  7923  exbtwnz  10288  rersqreu  11079  divalglemeunn  11968  divalglemeuneg  11970  bezoutlemeu  12050  pw2dvdseu  12212  ismgmid  12865  mndideu  12911  dedekindeu  14595  dedekindicclemicc  14604