Theorem reu5 2690

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 2073	. 2 |- ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
2		df-reu 2462	. 2 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		df-rex 2461	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4		df-rmo 2463	. . 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 1492   E!weu 2026   E*wmo 2027   e. wcel 2148   E.wrex 2456   E!wreu 2457   E*wrmo 2458

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-rex 2461  df-reu 2462  df-rmo 2463

This theorem is referenced by:  reurex  2691  reurmo  2692  reu4  2932  reueq  2937  reusv1  4459  fncnv  5283  moriotass  5859  supeuti  6993  infeuti  7028  lteupri  7616  elrealeu  7828  rereceu  7888  exbtwnz  10251  rersqreu  11037  divalglemeunn  11926  divalglemeuneg  11928  bezoutlemeu  12008  pw2dvdseu  12168  ismgmid  12796  mndideu  12827  dedekindeu  14104  dedekindicclemicc  14113