MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimiva Unicode version

Theorem rexlimiva 2663
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
Hypothesis
Ref Expression
rexlimiva.1  |-  ( ( x  e.  A  /\  ph )  ->  ps )
Assertion
Ref Expression
rexlimiva  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimiva
StepHypRef Expression
1 rexlimiva.1 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ps )
21ex 423 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2662 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1685   E.wrex 2545
This theorem is referenced by:  unon  4621  tfrlem16  6405  oawordeulem  6548  nneob  6646  ominf  7071  unfilem1  7117  pwfi  7147  fival  7162  elfi2  7164  fi0  7169  fiin  7171  finnum  7577  dif1card  7634  fseqenlem2  7648  dfac8alem  7652  alephfp  7731  cflim2  7885  isfin1-3  8008  fin67  8017  isfin7-2  8018  axdc3lem  8072  axdc3lem2  8073  iunfo  8157  iundom2g  8158  winainflem  8311  rankcf  8395  map2psrpr  8728  supsrlem  8729  1re  8833  00id  8983  addid1  8988  om2uzrani  11011  uzrdgfni  11017  wrdf  11415  rexanuz  11825  r19.2uz  11831  fsum2dlem  12229  fsumcom2  12233  0dvds  12545  ppttop  16740  epttop  16742  neips  16846  lmmo  17104  2ndctop  17169  2ndcsep  17181  fbncp  17530  fgcl  17569  filuni  17576  tgioo  18298  zcld  18315  elovolm  18830  nulmbl2  18890  ellimc3  19225  limcflf  19227  pilem3  19825  perfect  20466  2vmadivsum  20686  selberg3lem2  20703  selberg4  20706  pntrsumbnd2  20712  pntrlog2bndlem3  20724  pntrlog2bndlem4  20725  pntpbnd  20733  pnt3  20757  norm1exi  21825  nmcexi  22602  lnconi  22609  pjssdif1i  22751  stri  22833  hstri  22841  stcltrthi  22854  shatomici  22934  trpredlem1  23634  elno  23704  noreson  23717  axcontlem12  24013  axcont  24014  lvsovso  25037  clscnc  25421  cover2  25769  prtlem16  26148  rexzrexnn0  26296  isnumbasgrplem2  26680  dgraalem  26761  bnj1398  28343  bnj1498  28370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator