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

Theorem rexlimiva 2768
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 424 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2767 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1717   E.wrex 2650
This theorem is referenced by:  unon  4751  tfrlem16  6590  oawordeulem  6733  nneob  6831  ominf  7257  unfilem1  7307  pwfi  7337  fival  7352  elfi2  7354  fi0  7360  fiin  7362  finnum  7768  dif1card  7825  fseqenlem2  7839  dfac8alem  7843  alephfp  7922  cflim2  8076  isfin1-3  8199  fin67  8208  isfin7-2  8209  axdc3lem  8263  axdc3lem2  8264  iunfo  8347  iundom2g  8348  winainflem  8501  rankcf  8585  map2psrpr  8918  supsrlem  8919  1re  9023  00id  9173  addid1  9178  om2uzrani  11219  uzrdgfni  11225  wrdf  11660  rexanuz  12076  r19.2uz  12082  fsum2dlem  12481  fsumcom2  12485  0dvds  12797  ppttop  16994  epttop  16996  neips  17100  lmmo  17366  2ndctop  17431  2ndcsep  17443  fbncp  17792  fgcl  17831  filuni  17838  tgioo  18698  zcld  18715  elovolm  19238  nulmbl2  19298  ellimc3  19633  limcflf  19635  pilem3  20236  perfect  20882  2vmadivsum  21102  selberg3lem2  21119  selberg4  21122  pntrsumbnd2  21128  pntrlog2bndlem3  21140  pntrlog2bndlem4  21141  pntpbnd  21149  pnt3  21173  norm1exi  22600  nmcexi  23377  lnconi  23384  pjssdif1i  23526  stri  23608  hstri  23616  stcltrthi  23629  shatomici  23709  isrnmeas  24350  dya2iocucvr  24428  sxbrsigalem1  24429  trpredlem1  25254  elno  25324  noreson  25338  axcontlem12  25628  axcont  25629  volsupnfl  25956  itg2addnclem  25957  itg2addnc  25959  cover2  26106  prtlem16  26409  rexzrexnn0  26555  isnumbasgrplem2  26938  dgraalem  27019  stirlinglem13  27503  stirlinglem14  27504  stirling  27506  bnj1398  28741  bnj1498  28768
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2654  df-rex 2655
  Copyright terms: Public domain W3C validator