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  stoweidlem27  26910  stoweidlem28  26911  stoweidlem52  26935  stoweidlem57  26940  stoweidlem59  26942  stoweidlem60  26943  stoweidlem61  26944  stoweidlem62  26945  lshpcmp  28082  lsatn0  28093  lsatcmp  28097  lsmsat  28102  lsatcv0  28125  l1cvpat  28148  eqlkr  28193  lshpkrlem1  28204  lshpkrlem6  28209  lfl1dim  28215  lfl1dim2N  28216  lkrss2N  28263  cvlcvr1  28433  athgt  28549  3dim2  28561  llnle  28611  llncmp  28615  llnmlplnN  28632  lplnle  28633  lplnnle2at  28634  llncvrlpln2  28650  llncvrlpln  28651  lplncmp  28655  lplnexllnN  28657  lvolnle3at  28675  lplncvrlvol2  28708  lplncvrlvol  28709  lvolcmp  28710  pointpsubN  28844  cdlemb  28887  paddasslem10  28922  pclfinN  28993  pclfinclN  29043  osumcllem11N  29059  pexmidlem4N  29066  pexmidlem8N  29070  lhprelat3N  29133  trlcnv  29258  trlator0  29264  trlid0  29269  trlnidatb  29270  cdlemd4  29294  cdleme17d3  29589  cdlemeg46gfre  29625  cdleme48gfv1  29629  cdleme50trn2  29644  trlord  29662  cdlemg5  29698  cdlemg6e  29715  trlco  29820  cdlemj3  29916  tendo0mul  29919  tendo0mulr  29920  tendoconid  29922  erngdv  30086  erngdv-rN  30094  diaelrnN  30139  diaintclN  30152  dia2dimlem6  30163  cdlemm10N  30212  dibintclN  30261  dihord6apre  30350  dihord5b  30353  dihord5apre  30356  dihmeetlem1N  30384  dihglblem5apreN  30385  dihglblem2N  30388  dihglblem3N  30389  dihglbcpreN  30394  dihatlat  30428  dihintcl  30438  lclkrlem2y  30625  lcfrvalsnN  30635  hgmaprnlem5N  30997
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