Theorem reu5 2726

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 2103	. 2 |- ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
2		df-reu 2493	. 2 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		df-rex 2492	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4		df-rmo 2494	. . 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 1516   E!weu 2055   E*wmo 2056   e. wcel 2178   E.wrex 2487   E!wreu 2488   E*wrmo 2489

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-rex 2492  df-reu 2493  df-rmo 2494

This theorem is referenced by:  reurex  2727  reurmo  2728  cbvreuw  2737  reu4  2974  reueq  2979  reusv1  4523  fncnv  5359  moriotass  5951  supeuti  7122  infeuti  7157  lteupri  7765  elrealeu  7977  rereceu  8037  exbtwnz  10430  rersqreu  11454  divalglemeunn  12347  divalglemeuneg  12349  bezoutlemeu  12443  pw2dvdseu  12605  ismgmid  13324  mndideu  13373  dedekindeu  15210  dedekindicclemicc  15219