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

Theorem rexlimdv 2830
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 1672 . 2  |-  F/ x ph
2 nfv 1672 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2828 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  rexlimdva  2831  rexlimdv3a  2833  rexlimdvw  2834  rexlimdvv  2837  elpwunsn  3905  trintss  4389  eldmrexrnb  5838  dffo3  5846  weniso  6032  ssorduni  6386  onint  6395  limuni3  6452  funcnvuni  6519  frxp  6671  smoiun  6808  tfrlem9  6830  oaordex  6985  oalimcl  6987  oaass  6988  omlimcl  7005  fisucdomOLD  7504  findcard3  7543  frfi  7545  unblem1  7552  ordiso2  7717  inf3lem3  7824  noinfepOLD  7854  r1sdom  7969  tz9.12lem3  7984  karden  8090  infxpenlem  8168  cardinfima  8255  iunfictbso  8272  dfac5  8286  cfflb  8416  cfcoflem  8429  cfcof  8431  fin23lem11  8474  fin23lem30  8499  fin1a2lem13  8569  axdc3lem2  8608  konigthlem  8720  alephval2  8724  pwcfsdom  8735  fpwwe2lem12  8796  tskuni  8938  axgroth6  8983  nqereu  9086  genpnmax  9164  ltaddpr  9191  recexsrlem  9258  mulgt0sr  9260  recexsr  9262  axrrecex  9318  axpre-sup  9324  addid1  9537  addid2  9540  recex  9956  zdiv  10700  btwnz  10732  lbzbi  10931  qbtwnre  11157  caubnd  12830  divalglem9  13588  unbenlem  13952  firest  14354  imasmnd2  15441  imasgrp2  15650  pmtrfrn  15944  pgpfi  16084  sylow2blem3  16101  imasrng  16646  lspsneq  17125  lspdisj  17128  unitg  18414  fctop  18450  cctop  18452  elcls  18519  elcls3  18529  subbascn  18700  cmpsublem  18844  cmpsub  18845  nllyidm  18935  ptpjopn  19027  fbfinnfr  19256  filin  19269  isfil2  19271  infil  19278  fgss2  19289  fgfil  19290  fgcl  19293  fgabs  19294  elfm2  19363  rnelfm  19368  fmfnfmlem2  19370  fmfnfmlem4  19372  fmco  19376  flffbas  19410  cnpflf2  19415  fclscf  19440  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  alexsubALT  19465  neibl  19918  met2ndc  19940  metcnp3  19957  icccmplem2  20242  xrge0tsms  20253  fgcfil  20624  volfiniun  20870  dyadmax  20920  dyadmbllem  20921  c1liplem1  21310  dgrlem  21582  axcontlem10  23042  usgrarnedg  23126  lpni  23489  grpoidinvlem3  23516  grpoidinvlem4  23517  grporcan  23531  grpoinvf  23550  nmosetre  23987  omlsii  24629  spansncol  24794  spansnss  24797  normcan  24802  spanunsni  24805  h1datomi  24807  nmopsetretALT  25090  nmfnsetre  25104  branmfn  25332  cnvbraval  25337  opsqrlem1  25367  superpos  25581  chjatom  25584  cvbr4i  25594  atomli  25609  xrge0tsmsd  26106  eulerpartlemgh  26609  dfon2lem6  27448  trpredrec  27549  colineardim1  27939  finminlem  28357  nn0prpwlem  28361  comppfsc  28423  neibastop2lem  28425  neibastop2  28426  fgmin  28435  heiborlem10  28563  prtlem15  28865  isnacs3  28891  jm2.26  29196  fnwe2lem2  29249  lnrfg  29320  hbtlem5  29329  climsuse  29627  stoweidlem27  29668  stoweidlem52  29693  stoweidlem59  29700  erclwwlksym  30330  erclwwlknsym  30346  islindeps2  30726  lshpcmp  32206  lsatn0  32217  lsatcmp  32221  lsmsat  32226  lsatcv0  32249  l1cvpat  32272  eqlkr  32317  lshpkrlem1  32328  lshpkrlem6  32333  lfl1dim  32339  lfl1dim2N  32340  lkrss2N  32387  athgt  32673  3dim2  32685  llnle  32735  llncmp  32739  lplnle  32757  lplnnle2at  32758  llncvrlpln2  32774  llncvrlpln  32775  lplncmp  32779  lplnexllnN  32781  lvolnle3at  32799  lplncvrlvol2  32832  lplncvrlvol  32833  lvolcmp  32834  pointpsubN  32968  pclfinN  33117  pclfinclN  33167  osumcllem11N  33183  pexmidlem4N  33190  lhprelat3N  33257  cdleme17d3  33713  cdlemeg46gfre  33749  cdleme48gfv1  33753  cdleme50trn2  33768  trlord  33786  cdlemg6e  33839  cdlemj3  34040  diaelrnN  34263  diaintclN  34276  dia2dimlem6  34287  cdlemm10N  34336  dibintclN  34385  dihord6apre  34474  dihord5b  34477  dihord5apre  34480  dihglblem5apreN  34509  dihglblem2N  34512  dihglblem3N  34513  dihglbcpreN  34518  dihintcl  34562  lclkrlem2y  34749  lcfrvalsnN  34759
  Copyright terms: Public domain W3C validator