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

Theorem rexlimdv 2821
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
rexlimdv.1  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimdv  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdv
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 nfv 1629 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2819 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  rexlimdva  2822  rexlimdv3a  2824  rexlimdvw  2825  rexlimdvv  2828  trintss  4310  elpwunsn  4749  ssorduni  4758  onint  4767  limuni3  4824  funcnvuni  5510  eldmrexrnb  5869  dffo3  5876  weniso  6067  frxp  6448  smoiun  6615  tfrlem9  6638  oaordex  6793  oalimcl  6795  oaass  6796  omlimcl  6813  fisucdomOLD  7304  findcard3  7342  frfi  7344  unblem1  7351  ordiso2  7476  inf3lem3  7577  noinfepOLD  7607  r1sdom  7692  tz9.12lem3  7707  karden  7811  infxpenlem  7887  cardinfima  7970  iunfictbso  7987  dfac5  8001  cfflb  8131  cfcoflem  8144  cfcof  8146  fin23lem11  8189  fin23lem30  8214  fin1a2lem13  8284  axdc3lem2  8323  konigthlem  8435  alephval2  8439  pwcfsdom  8450  fpwwe2lem12  8508  tskuni  8650  axgroth6  8695  nqereu  8798  genpnmax  8876  ltaddpr  8903  recexsrlem  8970  mulgt0sr  8972  recexsr  8974  axrrecex  9030  axpre-sup  9036  addid1  9238  addid2  9241  recex  9646  zdiv  10332  btwnz  10364  lbzbi  10556  qbtwnre  10777  caubnd  12154  divalglem9  12913  unbenlem  13268  firest  13652  imasmnd2  14724  imasgrp2  14925  pgpfi  15231  sylow2blem3  15248  imasrng  15717  lspsneq  16186  lspdisj  16189  unitg  17024  fctop  17060  cctop  17062  elcls  17129  elcls3  17139  subbascn  17310  cmpsublem  17454  cmpsub  17455  nllyidm  17544  ptpjopn  17636  fbfinnfr  17865  filin  17878  isfil2  17880  infil  17887  fgss2  17898  fgfil  17899  fgcl  17902  fgabs  17903  elfm2  17972  rnelfm  17977  fmfnfmlem2  17979  fmfnfmlem4  17981  fmco  17985  flffbas  18019  cnpflf2  18024  fclscf  18049  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALTlem4  18073  alexsubALT  18074  neibl  18523  met2ndc  18545  metcnp3  18562  icccmplem2  18846  xrge0tsms  18857  fgcfil  19216  volfiniun  19433  dyadmax  19482  dyadmbllem  19483  c1liplem1  19872  dgrlem  20140  usgrarnedg  21396  lpni  21759  grpoidinvlem3  21786  grpoidinvlem4  21787  grporcan  21801  grpoinvf  21820  nmosetre  22257  omlsii  22897  spansncol  23062  spansnss  23065  normcan  23070  spanunsni  23073  h1datomi  23075  nmopsetretALT  23358  nmfnsetre  23372  branmfn  23600  cnvbraval  23605  opsqrlem1  23635  superpos  23849  chjatom  23852  cvbr4i  23862  atomli  23877  xrge0tsmsd  24215  dfon2lem6  25407  trpredrec  25508  axcontlem10  25904  colineardim1  25987  finminlem  26312  nn0prpwlem  26316  comppfsc  26378  neibastop2lem  26380  neibastop2  26381  fgmin  26390  heiborlem10  26520  prtlem15  26715  isnacs3  26755  jm2.26  27064  fnwe2lem2  27117  lnrfg  27291  hbtlem5  27300  pmtrfrn  27368  climsuse  27701  stoweidlem27  27743  stoweidlem52  27768  stoweidlem59  27775  lshpcmp  29723  lsatn0  29734  lsatcmp  29738  lsmsat  29743  lsatcv0  29766  l1cvpat  29789  eqlkr  29834  lshpkrlem1  29845  lshpkrlem6  29850  lfl1dim  29856  lfl1dim2N  29857  lkrss2N  29904  athgt  30190  3dim2  30202  llnle  30252  llncmp  30256  lplnle  30274  lplnnle2at  30275  llncvrlpln2  30291  llncvrlpln  30292  lplncmp  30296  lplnexllnN  30298  lvolnle3at  30316  lplncvrlvol2  30349  lplncvrlvol  30350  lvolcmp  30351  pointpsubN  30485  pclfinN  30634  pclfinclN  30684  osumcllem11N  30700  pexmidlem4N  30707  lhprelat3N  30774  cdleme17d3  31230  cdlemeg46gfre  31266  cdleme48gfv1  31270  cdleme50trn2  31285  trlord  31303  cdlemg6e  31356  cdlemj3  31557  diaelrnN  31780  diaintclN  31793  dia2dimlem6  31804  cdlemm10N  31853  dibintclN  31902  dihord6apre  31991  dihord5b  31994  dihord5apre  31997  dihglblem5apreN  32026  dihglblem2N  32029  dihglblem3N  32030  dihglbcpreN  32035  dihintcl  32079  lclkrlem2y  32266  lcfrvalsnN  32276
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator