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

Theorem rexlimdv 2667
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 1606 . 2  |-  F/ x ph
2 nfv 1606 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2665 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685   E.wrex 2545
This theorem is referenced by:  rexlimdva  2668  rexlimdv3a  2670  rexlimdvw  2671  rexlimdvv  2674  trintss  4130  tz7.7  4417  elpwunsn  4567  ssorduni  4576  onint  4585  limuni3  4642  funcnvuni  5282  dffo3  5636  isofrlem  5798  weniso  5813  frxp  6186  smoiun  6373  tfrlem9  6396  oaordex  6551  oalimcl  6553  oaass  6554  omlimcl  6571  fisucdomOLD  7061  findcard3  7095  frfi  7097  unblem1  7104  marypha1lem  7181  ordiso2  7225  inf3lem3  7326  noinfepOLD  7356  r1sdom  7441  tz9.12lem3  7456  karden  7560  infxpenlem  7636  cardaleph  7711  cardinfima  7719  iunfictbso  7736  dfac5  7750  cfflb  7880  cfcoflem  7893  coftr  7894  cfcof  7895  fin23lem11  7938  fin23lem30  7963  fin1a2lem13  8033  axdc3lem2  8072  konigthlem  8185  alephval2  8189  pwcfsdom  8200  fpwwe2lem12  8258  tskuni  8400  grur1  8437  axgroth6  8445  inaprc  8453  nqereu  8548  genpnmax  8626  prlem934  8652  ltaddpr  8653  ltexprlem7  8661  reclem3pr  8668  recexsrlem  8720  mulgt0sr  8722  recexsr  8724  axrrecex  8780  axpre-sup  8786  00id  8982  mul02lem1  8983  addid1  8987  addid2  8990  recex  9395  receu  9408  zdiv  10077  btwnz  10109  lbzbi  10301  qbtwnre  10520  caubnd  11836  caucvgb  12146  dvdsval2  12528  divalglem9  12594  unbenlem  12949  firest  13331  isacs3lem  14263  imasmnd2  14403  imasgrp2  14604  pgpfi  14910  sylow2blem3  14927  imasrng  15396  lspsneq  15869  lspdisj  15872  drngnidl  15975  unitg  16699  tgcl  16701  fctop  16735  cctop  16737  elcls  16804  elcls3  16814  restcls  16905  restntr  16906  subbascn  16978  cnpnei  16987  cmpsublem  17120  cmpsub  17121  2ndc1stc  17171  2ndcctbss  17175  nllyidm  17209  ptpjopn  17300  fbfinnfr  17530  filin  17543  isfil2  17545  infil  17552  fbasfip  17557  fgss2  17563  fgfil  17564  fgcl  17567  fgabs  17568  fbasrn  17573  elfm2  17637  elfm3  17639  rnelfmlem  17641  rnelfm  17642  fmfnfmlem2  17644  fmfnfmlem4  17646  fmco  17650  flffbas  17684  cnpflf2  17689  fclscf  17714  alexsubALTlem2  17736  alexsubALTlem3  17737  alexsubALTlem4  17738  alexsubALT  17739  neibl  18041  met2ndc  18063  metcnp3  18080  icccmplem2  18322  xrge0tsms  18333  fgcfil  18691  volfiniun  18898  dyadmax  18947  dyadmbllem  18948  c1liplem1  19337  dgrlem  19605  aaliou3lem8  19719  aaliou3lem9  19724  lpni  20838  grpoidinvlem3  20865  grpoidinvlem4  20866  grporcan  20880  grpoinvf  20899  nmosetre  21334  omlsii  21974  spansncol  22139  spansneleq  22141  spansnss  22142  normcan  22147  spanunsni  22150  h1datomi  22152  chscllem3  22210  nmopsetretALT  22435  nmfnsetre  22449  branmfn  22677  cnvbraval  22682  opsqrlem1  22712  superpos  22926  chjatom  22929  cvbr4i  22939  atomli  22954  dfon2lem6  23545  trpredrec  23642  axdenselem5  23740  axfelem6  23752  axfelem19  23765  brbtwn2  23940  colinearalg  23945  axcontlem10  24008  colineardim1  24091  btwnconn1lem13  24129  outsidele  24162  grpodivfo  24773  trran2  24792  ltrran2  24802  trran  25013  finminlem  25630  nn0prpwlem  25637  reftr  25688  comppfsc  25706  neibastop2lem  25708  neibastop2  25709  fgmin  25718  tailfb  25725  heiborlem8  25941  heiborlem10  25943  unichnidl  26055  prtlem15  26142  isnacs3  26184  acongrep  26466  jm2.26  26494  jm2.27b  26498  fnwe2lem2  26547  lnrfg  26722  hbtlem5  26731  pmtrfrn  26799  stoweidlem27  27175  stoweidlem28  27176  stoweidlem52  27200  stoweidlem57  27205  stoweidlem59  27207  stoweidlem60  27208  stoweidlem61  27209  stoweidlem62  27210  lshpcmp  28445  lsatn0  28456  lsatcmp  28460  lsmsat  28465  lsatcv0  28488  l1cvpat  28511  eqlkr  28556  lshpkrlem1  28567  lshpkrlem6  28572  lfl1dim  28578  lfl1dim2N  28579  lkrss2N  28626  cvlcvr1  28796  athgt  28912  3dim2  28924  llnle  28974  llncmp  28978  llnmlplnN  28995  lplnle  28996  lplnnle2at  28997  llncvrlpln2  29013  llncvrlpln  29014  lplncmp  29018  lplnexllnN  29020  lvolnle3at  29038  lplncvrlvol2  29071  lplncvrlvol  29072  lvolcmp  29073  pointpsubN  29207  cdlemb  29250  paddasslem10  29285  pclfinN  29356  pclfinclN  29406  osumcllem11N  29422  pexmidlem4N  29429  pexmidlem8N  29433  lhprelat3N  29496  trlcnv  29621  trlator0  29627  trlid0  29632  trlnidatb  29633  cdlemd4  29657  cdleme17d3  29952  cdlemeg46gfre  29988  cdleme48gfv1  29992  cdleme50trn2  30007  trlord  30025  cdlemg5  30061  cdlemg6e  30078  trlco  30183  cdlemj3  30279  tendo0mul  30282  tendo0mulr  30283  tendoconid  30285  erngdv  30449  erngdv-rN  30457  diaelrnN  30502  diaintclN  30515  dia2dimlem6  30526  cdlemm10N  30575  dibintclN  30624  dihord6apre  30713  dihord5b  30716  dihord5apre  30719  dihmeetlem1N  30747  dihglblem5apreN  30748  dihglblem2N  30751  dihglblem3N  30752  dihglbcpreN  30757  dihatlat  30791  dihintcl  30801  lclkrlem2y  30988  lcfrvalsnN  30998  hgmaprnlem5N  31360
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator