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

Theorem rexlimiva 2769
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 2768 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1717   E.wrex 2651
This theorem is referenced by:  unon  4752  tfrlem16  6591  oawordeulem  6734  nneob  6832  ominf  7258  unfilem1  7308  pwfi  7338  fival  7353  elfi2  7355  fi0  7361  fiin  7363  finnum  7769  dif1card  7826  fseqenlem2  7840  dfac8alem  7844  alephfp  7923  cflim2  8077  isfin1-3  8200  fin67  8209  isfin7-2  8210  axdc3lem  8264  axdc3lem2  8265  iunfo  8348  iundom2g  8349  winainflem  8502  rankcf  8586  map2psrpr  8919  supsrlem  8920  1re  9024  00id  9174  addid1  9179  om2uzrani  11220  uzrdgfni  11226  wrdf  11661  rexanuz  12077  r19.2uz  12083  fsum2dlem  12482  fsumcom2  12486  0dvds  12798  ppttop  16995  epttop  16997  neips  17101  lmmo  17367  2ndctop  17432  2ndcsep  17444  fbncp  17793  fgcl  17832  filuni  17839  tgioo  18699  zcld  18716  elovolm  19239  nulmbl2  19299  ellimc3  19634  limcflf  19636  pilem3  20237  perfect  20883  2vmadivsum  21103  selberg3lem2  21120  selberg4  21123  pntrsumbnd2  21129  pntrlog2bndlem3  21141  pntrlog2bndlem4  21142  pntpbnd  21150  pnt3  21174  norm1exi  22601  nmcexi  23378  lnconi  23385  pjssdif1i  23527  stri  23609  hstri  23617  stcltrthi  23630  shatomici  23710  isrnmeas  24351  dya2iocucvr  24429  sxbrsigalem1  24430  trpredlem1  25255  elno  25325  noreson  25339  axcontlem12  25629  axcont  25630  volsupnfl  25957  itg2addnclem  25958  itg2addnc  25960  cover2  26107  prtlem16  26410  rexzrexnn0  26556  isnumbasgrplem2  26939  dgraalem  27020  stirlinglem13  27504  stirlinglem14  27505  stirling  27507  bnj1398  28742  bnj1498  28769
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 2655  df-rex 2656
  Copyright terms: Public domain W3C validator