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

Theorem rexlimiva 2789
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 2788 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   E.wrex 2671
This theorem is referenced by:  unon  4774  tfrlem16  6617  oawordeulem  6760  nneob  6858  ominf  7284  unfilem1  7334  pwfi  7364  fival  7379  elfi2  7381  fi0  7387  fiin  7389  finnum  7795  dif1card  7852  fseqenlem2  7866  dfac8alem  7870  alephfp  7949  cflim2  8103  isfin1-3  8226  fin67  8235  isfin7-2  8236  axdc3lem  8290  axdc3lem2  8291  iunfo  8374  iundom2g  8375  winainflem  8528  rankcf  8612  map2psrpr  8945  supsrlem  8946  1re  9050  00id  9201  addid1  9206  om2uzrani  11251  uzrdgfni  11257  wrdf  11692  rexanuz  12108  r19.2uz  12114  fsum2dlem  12513  fsumcom2  12517  0dvds  12829  ppttop  17030  epttop  17032  neips  17136  lmmo  17402  2ndctop  17467  2ndcsep  17479  fbncp  17828  fgcl  17867  filuni  17874  tgioo  18784  zcld  18801  elovolm  19328  nulmbl2  19388  ellimc3  19723  limcflf  19725  pilem3  20326  perfect  20972  2vmadivsum  21192  selberg3lem2  21209  selberg4  21212  pntrsumbnd2  21218  pntrlog2bndlem3  21230  pntrlog2bndlem4  21231  pntpbnd  21239  pnt3  21263  norm1exi  22709  nmcexi  23486  lnconi  23493  pjssdif1i  23635  stri  23717  hstri  23725  stcltrthi  23738  shatomici  23818  isrnmeas  24511  dya2iocucvr  24591  sxbrsigalem1  24592  fprod2dlem  25261  fprodcom2  25265  trpredlem1  25448  elno  25518  noreson  25532  axcontlem12  25822  axcont  25823  mblfinlem2  26148  ismblfin  26150  volsupnfl  26154  itg2addnclem  26159  itg2addnc  26162  cover2  26309  prtlem16  26612  rexzrexnn0  26758  isnumbasgrplem2  27141  dgraalem  27222  stirlinglem13  27706  stirlinglem14  27707  stirling  27709  bnj1398  29113  bnj1498  29140
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 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675  df-rex 2676
  Copyright terms: Public domain W3C validator