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  4506  fncnv  5341  moriotass  5930  supeuti  7098  infeuti  7133  lteupri  7732  elrealeu  7944  rereceu  8004  exbtwnz  10395  rersqreu  11372  divalglemeunn  12265  divalglemeuneg  12267  bezoutlemeu  12361  pw2dvdseu  12523  ismgmid  13242  mndideu  13291  dedekindeu  15128  dedekindicclemicc  15137