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

Theorem rexlimdv 2946
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 1674 . 2  |-  F/ x ph
2 nfv 1674 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2944 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   E.wrex 2800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2804  df-rex 2805
This theorem is referenced by:  rexlimdva  2947  rexlimdv3a  2949  rexlimdvw  2950  rexlimdvv  2953  elpwunsn  4026  trintss  4510  eldmrexrnb  5960  dffo3  5968  weniso  6155  ssorduni  6508  onint  6517  limuni3  6574  funcnvuni  6641  frxp  6793  smoiun  6933  tfrlem9  6955  oaordex  7108  oalimcl  7110  oaass  7111  omlimcl  7128  fisucdomOLD  7628  findcard3  7667  frfi  7669  unblem1  7676  ordiso2  7841  inf3lem3  7948  noinfepOLD  7978  r1sdom  8093  tz9.12lem3  8108  karden  8214  infxpenlem  8292  cardinfima  8379  iunfictbso  8396  dfac5  8410  cfflb  8540  cfcoflem  8553  cfcof  8555  fin23lem11  8598  fin23lem30  8623  fin1a2lem13  8693  axdc3lem2  8732  konigthlem  8844  alephval2  8848  pwcfsdom  8859  fpwwe2lem12  8920  tskuni  9062  axgroth6  9107  nqereu  9210  genpnmax  9288  ltaddpr  9315  recexsrlem  9382  mulgt0sr  9384  recexsr  9386  axrrecex  9442  axpre-sup  9448  addid1  9661  addid2  9664  recex  10080  zdiv  10824  btwnz  10856  lbzbi  11055  qbtwnre  11281  caubnd  12965  divalglem9  13724  unbenlem  14088  firest  14491  imasmnd2  15578  imasgrp2  15790  pmtrfrn  16084  pgpfi  16226  sylow2blem3  16243  imasrng  16835  lspsneq  17327  lspdisj  17330  unitg  18705  fctop  18741  cctop  18743  elcls  18810  elcls3  18820  subbascn  18991  cmpsublem  19135  cmpsub  19136  nllyidm  19226  ptpjopn  19318  fbfinnfr  19547  filin  19560  isfil2  19562  infil  19569  fgss2  19580  fgfil  19581  fgcl  19584  fgabs  19585  elfm2  19654  rnelfm  19659  fmfnfmlem2  19661  fmfnfmlem4  19663  fmco  19667  flffbas  19701  cnpflf2  19706  fclscf  19731  alexsubALTlem2  19753  alexsubALTlem3  19754  alexsubALTlem4  19755  alexsubALT  19756  neibl  20209  met2ndc  20231  metcnp3  20248  icccmplem2  20533  xrge0tsms  20544  fgcfil  20915  volfiniun  21162  dyadmax  21212  dyadmbllem  21213  c1liplem1  21602  dgrlem  21831  axcontlem10  23372  usgrarnedg  23456  lpni  23819  grpoidinvlem3  23846  grpoidinvlem4  23847  grporcan  23861  grpoinvf  23880  nmosetre  24317  omlsii  24959  spansncol  25124  spansnss  25127  normcan  25132  spanunsni  25135  h1datomi  25137  nmopsetretALT  25420  nmfnsetre  25434  branmfn  25662  cnvbraval  25667  opsqrlem1  25697  superpos  25911  chjatom  25914  cvbr4i  25924  atomli  25939  xrge0tsmsd  26399  eulerpartlemgh  26906  dfon2lem6  27746  trpredrec  27847  colineardim1  28237  finminlem  28662  nn0prpwlem  28666  comppfsc  28728  neibastop2lem  28730  neibastop2  28731  fgmin  28740  heiborlem10  28868  prtlem15  29169  isnacs3  29195  jm2.26  29500  fnwe2lem2  29553  lnrfg  29624  hbtlem5  29633  climsuse  29930  stoweidlem27  29971  stoweidlem59  30003  erclwwlksym  30633  erclwwlknsym  30649  islindeps2  31150  lshpcmp  32972  lsatn0  32983  lsatcmp  32987  lsmsat  32992  lsatcv0  33015  l1cvpat  33038  eqlkr  33083  lshpkrlem1  33094  lshpkrlem6  33099  lfl1dim  33105  lfl1dim2N  33106  lkrss2N  33153  athgt  33439  3dim2  33451  llnle  33501  llncmp  33505  lplnle  33523  lplnnle2at  33524  llncvrlpln2  33540  llncvrlpln  33541  lplncmp  33545  lplnexllnN  33547  lvolnle3at  33565  lplncvrlvol2  33598  lplncvrlvol  33599  lvolcmp  33600  pointpsubN  33734  pclfinN  33883  pclfinclN  33933  osumcllem11N  33949  pexmidlem4N  33956  lhprelat3N  34023  cdleme17d3  34479  cdlemeg46gfre  34515  cdleme48gfv1  34519  cdleme50trn2  34534  trlord  34552  cdlemg6e  34605  cdlemj3  34806  diaelrnN  35029  diaintclN  35042  dia2dimlem6  35053  cdlemm10N  35102  dibintclN  35151  dihord6apre  35240  dihord5b  35243  dihord5apre  35246  dihglblem5apreN  35275  dihglblem2N  35278  dihglblem3N  35279  dihglbcpreN  35284  dihintcl  35328  lclkrlem2y  35515  lcfrvalsnN  35525
  Copyright terms: Public domain W3C validator