Theorem reu5 3159

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 2496	. 2 |- ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E* x ( x e. A /\ ph ) ) )
2		df-reu 2919	. 2 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		df-rex 2918	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4		df-rmo 2920	. . 3 |- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
5	3, 4	anbi12i 733	. 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 292	1 |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704   e. wcel 1990   E!weu 2470   E*wmo 2471   E.wrex 2913   E!wreu 2914   E*wrmo 2915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-eu 2474  df-mo 2475  df-rex 2918  df-reu 2919  df-rmo 2920

This theorem is referenced by:  reurex  3160  reurmo  3161  reu4  3400  reueq  3404  reusv1  4866  reusv1OLD  4867  wereu  5110  wereu2  5111  fncnv  5962  moriotass  6640  supeu  8360  infeu  8402  resqreu  13993  sqrtneg  14008  sqreu  14100  catideu  16336  poslubd  17148  ismgmid  17264  mndideu  17304  evlseu  19516  frlmup4  20140  ply1divalg  23897  tglinethrueu  25534  foot  25614  mideu  25630  nbusgredgeu  26268  pjhtheu  28253  pjpreeq  28257  cnlnadjeui  28936  cvmliftlem14  31279  cvmlift2lem13  31297  cvmlift3  31310  nosupno  31849  nosupbday  31851  nosupbnd1  31860  nosupbnd2  31862  linethrueu  32263  phpreu  33393  poimirlem18  33427  poimirlem21  33430  2reu5a  41177  reuan  41180  2reurex  41181  2rexreu  41185  2reu1  41186