Theorem reu5 2723

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 2101	. 2 |- ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
2		df-reu 2491	. 2 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		df-rex 2490	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4		df-rmo 2492	. . 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 1515   E!weu 2054   E*wmo 2055   e. wcel 2176   E.wrex 2485   E!wreu 2486   E*wrmo 2487

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  df-rex 2490  df-reu 2491  df-rmo 2492

This theorem is referenced by:  reurex  2724  reurmo  2725  reu4  2967  reueq  2972  reusv1  4505  fncnv  5340  moriotass  5928  supeuti  7096  infeuti  7131  lteupri  7730  elrealeu  7942  rereceu  8002  exbtwnz  10393  rersqreu  11339  divalglemeunn  12232  divalglemeuneg  12234  bezoutlemeu  12328  pw2dvdseu  12490  ismgmid  13209  mndideu  13258  dedekindeu  15095  dedekindicclemicc  15104