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

Theorem rexlimdv 2666
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 1605 . 2  |-  F/ x ph
2 nfv 1605 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2664 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rexlimdva  2667  rexlimdv3a  2669  rexlimdvw  2670  rexlimdvv  2673  trintss  4129  tz7.7  4418  elpwunsn  4568  ssorduni  4577  onint  4586  limuni3  4643  funcnvuni  5317  dffo3  5675  isofrlem  5837  weniso  5852  frxp  6225  smoiun  6378  tfrlem9  6401  oaordex  6556  oalimcl  6558  oaass  6559  omlimcl  6576  fisucdomOLD  7066  findcard3  7100  frfi  7102  unblem1  7109  marypha1lem  7186  ordiso2  7230  inf3lem3  7331  noinfepOLD  7361  r1sdom  7446  tz9.12lem3  7461  karden  7565  infxpenlem  7641  cardaleph  7716  cardinfima  7724  iunfictbso  7741  dfac5  7755  cfflb  7885  cfcoflem  7898  coftr  7899  cfcof  7900  fin23lem11  7943  fin23lem30  7968  fin1a2lem13  8038  axdc3lem2  8077  konigthlem  8190  alephval2  8194  pwcfsdom  8205  fpwwe2lem12  8263  tskuni  8405  grur1  8442  axgroth6  8450  inaprc  8458  nqereu  8553  genpnmax  8631  prlem934  8657  ltaddpr  8658  ltexprlem7  8666  reclem3pr  8673  recexsrlem  8725  mulgt0sr  8727  recexsr  8729  axrrecex  8785  axpre-sup  8791  00id  8987  mul02lem1  8988  addid1  8992  addid2  8995  recex  9400  receu  9413  zdiv  10082  btwnz  10114  lbzbi  10306  qbtwnre  10526  caubnd  11842  caucvgb  12152  dvdsval2  12534  divalglem9  12600  unbenlem  12955  firest  13337  isacs3lem  14269  imasmnd2  14409  imasgrp2  14610  pgpfi  14916  sylow2blem3  14933  imasrng  15402  lspsneq  15875  lspdisj  15878  drngnidl  15981  unitg  16705  tgcl  16707  fctop  16741  cctop  16743  elcls  16810  elcls3  16820  restcls  16911  restntr  16912  subbascn  16984  cnpnei  16993  cmpsublem  17126  cmpsub  17127  2ndc1stc  17177  2ndcctbss  17181  nllyidm  17215  ptpjopn  17306  fbfinnfr  17536  filin  17549  isfil2  17551  infil  17558  fbasfip  17563  fgss2  17569  fgfil  17570  fgcl  17573  fgabs  17574  fbasrn  17579  elfm2  17643  elfm3  17645  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmco  17656  flffbas  17690  cnpflf2  17695  fclscf  17720  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  neibl  18047  met2ndc  18069  metcnp3  18086  icccmplem2  18328  xrge0tsms  18339  fgcfil  18697  volfiniun  18904  dyadmax  18953  dyadmbllem  18954  c1liplem1  19343  dgrlem  19611  aaliou3lem8  19725  aaliou3lem9  19730  lpni  20846  grpoidinvlem3  20873  grpoidinvlem4  20874  grporcan  20888  grpoinvf  20907  nmosetre  21342  omlsii  21982  spansncol  22147  spansneleq  22149  spansnss  22150  normcan  22155  spanunsni  22158  h1datomi  22160  chscllem3  22218  nmopsetretALT  22443  nmfnsetre  22457  branmfn  22685  cnvbraval  22690  opsqrlem1  22720  superpos  22934  chjatom  22937  cvbr4i  22947  atomli  22962  xreceu  23105  xrge0tsmsd  23382  esumcst  23436  dstfrvunirn  23675  dfon2lem6  24144  trpredrec  24241  nodenselem5  24339  nobndlem6  24351  brbtwn2  24533  colinearalg  24538  axcontlem10  24601  colineardim1  24684  btwnconn1lem13  24722  outsidele  24755  grpodivfo  25374  trran2  25393  ltrran2  25403  trran  25614  finminlem  26231  nn0prpwlem  26238  reftr  26289  comppfsc  26307  neibastop2lem  26309  neibastop2  26310  fgmin  26319  tailfb  26326  heiborlem8  26542  heiborlem10  26544  unichnidl  26656  prtlem15  26743  isnacs3  26785  acongrep  27067  jm2.26  27095  jm2.27b  27099  fnwe2lem2  27148  lnrfg  27323  hbtlem5  27332  pmtrfrn  27400  stoweidlem27  27776  stoweidlem28  27777  stoweidlem52  27801  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  stoweidlem61  27810  stoweidlem62  27811  lshpcmp  29178  lsatn0  29189  lsatcmp  29193  lsmsat  29198  lsatcv0  29221  l1cvpat  29244  eqlkr  29289  lshpkrlem1  29300  lshpkrlem6  29305  lfl1dim  29311  lfl1dim2N  29312  lkrss2N  29359  cvlcvr1  29529  athgt  29645  3dim2  29657  llnle  29707  llncmp  29711  llnmlplnN  29728  lplnle  29729  lplnnle2at  29730  llncvrlpln2  29746  llncvrlpln  29747  lplncmp  29751  lplnexllnN  29753  lvolnle3at  29771  lplncvrlvol2  29804  lplncvrlvol  29805  lvolcmp  29806  pointpsubN  29940  cdlemb  29983  paddasslem10  30018  pclfinN  30089  pclfinclN  30139  osumcllem11N  30155  pexmidlem4N  30162  pexmidlem8N  30166  lhprelat3N  30229  trlcnv  30354  trlator0  30360  trlid0  30365  trlnidatb  30366  cdlemd4  30390  cdleme17d3  30685  cdlemeg46gfre  30721  cdleme48gfv1  30725  cdleme50trn2  30740  trlord  30758  cdlemg5  30794  cdlemg6e  30811  trlco  30916  cdlemj3  31012  tendo0mul  31015  tendo0mulr  31016  tendoconid  31018  erngdv  31182  erngdv-rN  31190  diaelrnN  31235  diaintclN  31248  dia2dimlem6  31259  cdlemm10N  31308  dibintclN  31357  dihord6apre  31446  dihord5b  31449  dihord5apre  31452  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem2N  31484  dihglblem3N  31485  dihglbcpreN  31490  dihatlat  31524  dihintcl  31534  lclkrlem2y  31721  lcfrvalsnN  31731  hgmaprnlem5N  32093
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator