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

Theorem rexlimdv 2628
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 2626 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2510
This theorem is referenced by:  rexlimdva  2629  rexlimdv3a  2631  rexlimdvw  2632  rexlimdvv  2635  trintss  4026  tz7.7  4311  elpwunsn  4459  ssorduni  4468  onint  4477  limuni3  4534  funcnvuni  5174  dffo3  5527  isofrlem  5689  weniso  5704  frxp  6077  smoiun  6264  tfrlem9  6287  oaordex  6442  oalimcl  6444  oaass  6445  omlimcl  6462  fisucdomOLD  6951  findcard3  6985  frfi  6987  unblem1  6994  marypha1lem  7070  ordiso2  7114  inf3lem3  7215  noinfepOLD  7245  r1sdom  7330  tz9.12lem3  7345  karden  7449  infxpenlem  7525  cardaleph  7600  cardinfima  7608  iunfictbso  7625  dfac5  7639  cfflb  7769  cfcoflem  7782  coftr  7783  cfcof  7784  fin23lem11  7827  fin23lem30  7852  fin1a2lem13  7922  axdc3lem2  7961  konigthlem  8070  alephval2  8074  pwcfsdom  8085  fpwwe2lem12  8143  tskuni  8285  grur1  8322  axgroth6  8330  inaprc  8338  nqereu  8433  genpnmax  8511  prlem934  8537  ltaddpr  8538  ltexprlem7  8546  reclem3pr  8553  recexsrlem  8605  mulgt0sr  8607  recexsr  8609  axrrecex  8665  axpre-sup  8671  00id  8867  mul02lem1  8868  addid1  8872  addid2  8875  recex  9280  receu  9293  zdiv  9961  btwnz  9993  lbzbi  10185  qbtwnre  10404  caubnd  11719  caucvgb  12029  divides2  12408  divalglem9  12474  unbenlem  12829  firest  13211  isacs3lem  14113  imasmnd2  14244  imasgrp2  14445  pgpfi  14751  sylow2blem3  14768  imasrng  15237  lspsneq  15710  lspdisj  15713  drngnidl  15813  unitg  16537  tgcl  16539  fctop  16573  cctop  16575  elcls  16642  elcls3  16652  restcls  16743  restntr  16744  subbascn  16816  cnpnei  16825  cmpsublem  16958  cmpsub  16959  2ndc1stc  17009  2ndcctbss  17013  nllyidm  17047  ptpjopn  17138  fbfinnfr  17368  filin  17381  isfil2  17383  infil  17390  fbasfip  17395  fgss2  17401  fgfil  17402  fgcl  17405  fgabs  17406  fbasrn  17411  elfm2  17475  elfm3  17477  rnelfmlem  17479  rnelfm  17480  fmfnfmlem2  17482  fmfnfmlem4  17484  fmco  17488  flffbas  17522  cnpflf2  17527  fclscf  17552  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  alexsubALT  17577  neibl  17879  met2ndc  17901  metcnp3  17918  icccmplem2  18160  xrge0tsms  18171  fgcfil  18529  volfiniun  18736  dyadmax  18785  dyadmbllem  18786  c1liplem1  19175  dgrlem  19443  aaliou3lem8  19557  aaliou3lem9  19562  lpni  20676  grpoidinvlem3  20703  grpoidinvlem4  20704  grporcan  20718  grpoinvf  20737  nmosetre  21172  omlsii  21812  spansncol  21977  spansneleq  21979  spansnss  21980  normcan  21985  spanunsni  21988  h1datomi  21990  chscllem3  22066  nmopsetretALT  22273  nmfnsetre  22287  branmfn  22515  cnvbraval  22520  opsqrlem1  22550  superpos  22764  chjatom  22767  cvbr4i  22777  atomli  22792  dfon2lem6  23312  trpredrec  23409  axdenselem5  23507  axfelem6  23519  axfelem19  23532  brbtwn2  23707  colinearalg  23712  axcontlem10  23775  colineardim1  23858  btwnconn1lem13  23896  outsidele  23929  grpodivfo  24540  trran2  24559  ltrran2  24569  trran  24780  finminlem  25397  nn0prpwlem  25404  reftr  25455  comppfsc  25473  neibastop2lem  25475  neibastop2  25476  fgmin  25485  tailfb  25492  heiborlem8  25708  heiborlem10  25710  unichnidl  25822  prtlem15  25909  isnacs3  25951  acongrep  26233  jm2.26  26261  jm2.27b  26265  fnwe2lem2  26314  lnrfg  26489  hbtlem5  26498  pmtrfrn  26566  lshpcmp  27867  lsatn0  27878  lsatcmp  27882  lsmsat  27887  lsatcv0  27910  l1cvpat  27933  eqlkr  27978  lshpkrlem1  27989  lshpkrlem6  27994  lfl1dim  28000  lfl1dim2N  28001  lkrss2N  28048  cvlcvr1  28218  athgt  28334  3dim2  28346  llnle  28396  llncmp  28400  llnmlplnN  28417  lplnle  28418  lplnnle2at  28419  llncvrlpln2  28435  llncvrlpln  28436  lplncmp  28440  lplnexllnN  28442  lvolnle3at  28460  lplncvrlvol2  28493  lplncvrlvol  28494  lvolcmp  28495  pointpsubN  28629  cdlemb  28672  paddasslem10  28707  pclfinN  28778  pclfinclN  28828  osumcllem11N  28844  pexmidlem4N  28851  pexmidlem8N  28855  lhprelat3N  28918  trlcnv  29043  trlator0  29049  trlid0  29054  trlnidatb  29055  cdlemd4  29079  cdleme17d3  29374  cdlemeg46gfre  29410  cdleme48gfv1  29414  cdleme50trn2  29429  trlord  29447  cdlemg5  29483  cdlemg6e  29500  trlco  29605  cdlemj3  29701  tendo0mul  29704  tendo0mulr  29705  tendoconid  29707  erngdv  29871  erngdv-rN  29879  diaelrnN  29924  diaintclN  29937  dia2dimlem6  29948  cdlemm10N  29997  dibintclN  30046  dihord6apre  30135  dihord5b  30138  dihord5apre  30141  dihmeetlem1N  30169  dihglblem5apreN  30170  dihglblem2N  30173  dihglblem3N  30174  dihglbcpreN  30179  dihatlat  30213  dihintcl  30223  lclkrlem2y  30410  lcfrvalsnN  30420  hgmaprnlem5N  30782
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator