Theorem reu5 2770

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 2134	. 2 |- ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
2		df-reu 2535	. 2 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		df-rex 2534	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4		df-rmo 2536	. . 3 |- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
5	3, 4	anbi12i 464	. 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 ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   E.wex 1545   E!weu 2086   E*wmo 2087   e. wcel 2209   E.wrex 2529   E!wreu 2530   E*wrmo 2531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-rex 2534  df-reu 2535  df-rmo 2536

This theorem is used by:  reurex  2771  reurmo  2772  cbvreuw  2781  reu4  3020  reueq  3025  reusv1  4606  fncnv  5450  moriotass  6072  supeuti  7340  infeuti  7375  lteupri  7990  elrealeu  8202  rereceu  8262  exbtwnz  10702  rersqreu  11816  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemeu  12809  pwbdvdseu  12972  ismgmid  13756  mndideu  13798  dedekindeu  15849  dedekindicclemicc  15858  ralsanmo  17359