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

Theorem rexlimdv 2639
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 2637 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  rexlimdva  2640  rexlimdv3a  2642  rexlimdvw  2643  rexlimdvv  2646  trintss  4089  tz7.7  4376  elpwunsn  4526  ssorduni  4535  onint  4544  limuni3  4601  funcnvuni  5241  dffo3  5595  isofrlem  5757  weniso  5772  frxp  6145  smoiun  6332  tfrlem9  6355  oaordex  6510  oalimcl  6512  oaass  6513  omlimcl  6530  fisucdomOLD  7020  findcard3  7054  frfi  7056  unblem1  7063  marypha1lem  7140  ordiso2  7184  inf3lem3  7285  noinfepOLD  7315  r1sdom  7400  tz9.12lem3  7415  karden  7519  infxpenlem  7595  cardaleph  7670  cardinfima  7678  iunfictbso  7695  dfac5  7709  cfflb  7839  cfcoflem  7852  coftr  7853  cfcof  7854  fin23lem11  7897  fin23lem30  7922  fin1a2lem13  7992  axdc3lem2  8031  konigthlem  8144  alephval2  8148  pwcfsdom  8159  fpwwe2lem12  8217  tskuni  8359  grur1  8396  axgroth6  8404  inaprc  8412  nqereu  8507  genpnmax  8585  prlem934  8611  ltaddpr  8612  ltexprlem7  8620  reclem3pr  8627  recexsrlem  8679  mulgt0sr  8681  recexsr  8683  axrrecex  8739  axpre-sup  8745  00id  8941  mul02lem1  8942  addid1  8946  addid2  8949  recex  9354  receu  9367  zdiv  10035  btwnz  10067  lbzbi  10259  qbtwnre  10478  caubnd  11793  caucvgb  12103  divides2  12482  divalglem9  12548  unbenlem  12903  firest  13285  isacs3lem  14217  imasmnd2  14357  imasgrp2  14558  pgpfi  14864  sylow2blem3  14881  imasrng  15350  lspsneq  15823  lspdisj  15826  drngnidl  15929  unitg  16653  tgcl  16655  fctop  16689  cctop  16691  elcls  16758  elcls3  16768  restcls  16859  restntr  16860  subbascn  16932  cnpnei  16941  cmpsublem  17074  cmpsub  17075  2ndc1stc  17125  2ndcctbss  17129  nllyidm  17163  ptpjopn  17254  fbfinnfr  17484  filin  17497  isfil2  17499  infil  17506  fbasfip  17511  fgss2  17517  fgfil  17518  fgcl  17521  fgabs  17522  fbasrn  17527  elfm2  17591  elfm3  17593  rnelfmlem  17595  rnelfm  17596  fmfnfmlem2  17598  fmfnfmlem4  17600  fmco  17604  flffbas  17638  cnpflf2  17643  fclscf  17668  alexsubALTlem2  17690  alexsubALTlem3  17691  alexsubALTlem4  17692  alexsubALT  17693  neibl  17995  met2ndc  18017  metcnp3  18034  icccmplem2  18276  xrge0tsms  18287  fgcfil  18645  volfiniun  18852  dyadmax  18901  dyadmbllem  18902  c1liplem1  19291  dgrlem  19559  aaliou3lem8  19673  aaliou3lem9  19678  lpni  20792  grpoidinvlem3  20819  grpoidinvlem4  20820  grporcan  20834  grpoinvf  20853  nmosetre  21288  omlsii  21928  spansncol  22093  spansneleq  22095  spansnss  22096  normcan  22101  spanunsni  22104  h1datomi  22106  chscllem3  22182  nmopsetretALT  22389  nmfnsetre  22403  branmfn  22631  cnvbraval  22636  opsqrlem1  22666  superpos  22880  chjatom  22883  cvbr4i  22893  atomli  22908  dfon2lem6  23499  trpredrec  23596  axdenselem5  23694  axfelem6  23706  axfelem19  23719  brbtwn2  23894  colinearalg  23899  axcontlem10  23962  colineardim1  24045  btwnconn1lem13  24083  outsidele  24116  grpodivfo  24727  trran2  24746  ltrran2  24756  trran  24967  finminlem  25584  nn0prpwlem  25591  reftr  25642  comppfsc  25660  neibastop2lem  25662  neibastop2  25663  fgmin  25672  tailfb  25679  heiborlem8  25895  heiborlem10  25897  unichnidl  26009  prtlem15  26096  isnacs3  26138  acongrep  26420  jm2.26  26448  jm2.27b  26452  fnwe2lem2  26501  lnrfg  26676  hbtlem5  26685  pmtrfrn  26753  stoweidlem27  27097  stoweidlem28  27098  stoweidlem52  27122  stoweidlem57  27127  stoweidlem59  27129  stoweidlem60  27130  stoweidlem61  27131  stoweidlem62  27132  lshpcmp  28329  lsatn0  28340  lsatcmp  28344  lsmsat  28349  lsatcv0  28372  l1cvpat  28395  eqlkr  28440  lshpkrlem1  28451  lshpkrlem6  28456  lfl1dim  28462  lfl1dim2N  28463  lkrss2N  28510  cvlcvr1  28680  athgt  28796  3dim2  28808  llnle  28858  llncmp  28862  llnmlplnN  28879  lplnle  28880  lplnnle2at  28881  llncvrlpln2  28897  llncvrlpln  28898  lplncmp  28902  lplnexllnN  28904  lvolnle3at  28922  lplncvrlvol2  28955  lplncvrlvol  28956  lvolcmp  28957  pointpsubN  29091  cdlemb  29134  paddasslem10  29169  pclfinN  29240  pclfinclN  29290  osumcllem11N  29306  pexmidlem4N  29313  pexmidlem8N  29317  lhprelat3N  29380  trlcnv  29505  trlator0  29511  trlid0  29516  trlnidatb  29517  cdlemd4  29541  cdleme17d3  29836  cdlemeg46gfre  29872  cdleme48gfv1  29876  cdleme50trn2  29891  trlord  29909  cdlemg5  29945  cdlemg6e  29962  trlco  30067  cdlemj3  30163  tendo0mul  30166  tendo0mulr  30167  tendoconid  30169  erngdv  30333  erngdv-rN  30341  diaelrnN  30386  diaintclN  30399  dia2dimlem6  30410  cdlemm10N  30459  dibintclN  30508  dihord6apre  30597  dihord5b  30600  dihord5apre  30603  dihmeetlem1N  30631  dihglblem5apreN  30632  dihglblem2N  30635  dihglblem3N  30636  dihglbcpreN  30641  dihatlat  30675  dihintcl  30685  lclkrlem2y  30872  lcfrvalsnN  30882  hgmaprnlem5N  31244
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 2521  df-rex 2522
  Copyright terms: Public domain W3C validator