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

Theorem rexlimiva 2827
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 425 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2826 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  unon  4814  tfrlem16  6657  oawordeulem  6800  nneob  6898  ominf  7324  unfilem1  7374  pwfi  7405  fival  7420  elfi2  7422  fi0  7428  fiin  7430  finnum  7840  dif1card  7897  fseqenlem2  7911  dfac8alem  7915  alephfp  7994  cflim2  8148  isfin1-3  8271  fin67  8280  isfin7-2  8281  axdc3lem  8335  axdc3lem2  8336  iunfo  8419  iundom2g  8420  winainflem  8573  rankcf  8657  map2psrpr  8990  supsrlem  8991  1re  9095  00id  9246  addid1  9251  om2uzrani  11297  uzrdgfni  11303  wrdf  11738  rexanuz  12154  r19.2uz  12160  fsum2dlem  12559  fsumcom2  12563  0dvds  12875  ppttop  17076  epttop  17078  neips  17182  lmmo  17449  2ndctop  17515  2ndcsep  17527  fbncp  17876  fgcl  17915  filuni  17922  tgioo  18832  zcld  18849  elovolm  19376  nulmbl2  19436  ellimc3  19771  limcflf  19773  pilem3  20374  perfect  21020  2vmadivsum  21240  selberg3lem2  21257  selberg4  21260  pntrsumbnd2  21266  pntrlog2bndlem3  21278  pntrlog2bndlem4  21279  pntpbnd  21287  pnt3  21311  norm1exi  22757  nmcexi  23534  lnconi  23541  pjssdif1i  23683  stri  23765  hstri  23773  stcltrthi  23786  shatomici  23866  isrnmeas  24559  dya2iocucvr  24639  sxbrsigalem1  24640  fprod2dlem  25309  fprodcom2  25313  trpredlem1  25510  elno  25606  noreson  25620  axcontlem12  25919  axcont  25920  mblfinlem3  26256  ismblfin  26258  volsupnfl  26262  dvtanlem  26267  itg2addnclem  26269  itg2addnc  26272  cover2  26428  prtlem16  26731  rexzrexnn0  26877  isnumbasgrplem2  27259  dgraalem  27340  stirlinglem13  27824  stirlinglem14  27825  stirling  27827  modprm0  28261  bnj1398  29476  bnj1498  29503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator