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

Theorem rexlimdv 2789
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 1626 . 2  |-  F/ x ph
2 nfv 1626 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2787 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  rexlimdva  2790  rexlimdv3a  2792  rexlimdvw  2793  rexlimdvv  2796  trintss  4278  elpwunsn  4716  ssorduni  4725  onint  4734  limuni3  4791  funcnvuni  5477  eldmrexrnb  5836  dffo3  5843  weniso  6034  frxp  6415  smoiun  6582  tfrlem9  6605  oaordex  6760  oalimcl  6762  oaass  6763  omlimcl  6780  fisucdomOLD  7271  findcard3  7309  frfi  7311  unblem1  7318  ordiso2  7440  inf3lem3  7541  noinfepOLD  7571  r1sdom  7656  tz9.12lem3  7671  karden  7775  infxpenlem  7851  cardinfima  7934  iunfictbso  7951  dfac5  7965  cfflb  8095  cfcoflem  8108  cfcof  8110  fin23lem11  8153  fin23lem30  8178  fin1a2lem13  8248  axdc3lem2  8287  konigthlem  8399  alephval2  8403  pwcfsdom  8414  fpwwe2lem12  8472  tskuni  8614  axgroth6  8659  nqereu  8762  genpnmax  8840  ltaddpr  8867  recexsrlem  8934  mulgt0sr  8936  recexsr  8938  axrrecex  8994  axpre-sup  9000  addid1  9202  addid2  9205  recex  9610  zdiv  10296  btwnz  10328  lbzbi  10520  qbtwnre  10741  caubnd  12117  divalglem9  12876  unbenlem  13231  firest  13615  imasmnd2  14687  imasgrp2  14888  pgpfi  15194  sylow2blem3  15211  imasrng  15680  lspsneq  16149  lspdisj  16152  unitg  16987  fctop  17023  cctop  17025  elcls  17092  elcls3  17102  subbascn  17272  cmpsublem  17416  cmpsub  17417  nllyidm  17505  ptpjopn  17597  fbfinnfr  17826  filin  17839  isfil2  17841  infil  17848  fgss2  17859  fgfil  17860  fgcl  17863  fgabs  17864  elfm2  17933  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmco  17946  flffbas  17980  cnpflf2  17985  fclscf  18010  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  neibl  18484  met2ndc  18506  metcnp3  18523  icccmplem2  18807  xrge0tsms  18818  fgcfil  19177  volfiniun  19394  dyadmax  19443  dyadmbllem  19444  c1liplem1  19833  dgrlem  20101  usgrarnedg  21357  lpni  21720  grpoidinvlem3  21747  grpoidinvlem4  21748  grporcan  21762  grpoinvf  21781  nmosetre  22218  omlsii  22858  spansncol  23023  spansnss  23026  normcan  23031  spanunsni  23034  h1datomi  23036  nmopsetretALT  23319  nmfnsetre  23333  branmfn  23561  cnvbraval  23566  opsqrlem1  23596  superpos  23810  chjatom  23813  cvbr4i  23823  atomli  23838  xrge0tsmsd  24176  dfon2lem6  25358  trpredrec  25455  axcontlem10  25816  colineardim1  25899  finminlem  26211  nn0prpwlem  26215  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  fgmin  26289  heiborlem10  26419  prtlem15  26614  isnacs3  26654  jm2.26  26963  fnwe2lem2  27016  lnrfg  27191  hbtlem5  27200  pmtrfrn  27268  climsuse  27601  stoweidlem27  27643  stoweidlem52  27668  stoweidlem59  27675  lshpcmp  29471  lsatn0  29482  lsatcmp  29486  lsmsat  29491  lsatcv0  29514  l1cvpat  29537  eqlkr  29582  lshpkrlem1  29593  lshpkrlem6  29598  lfl1dim  29604  lfl1dim2N  29605  lkrss2N  29652  athgt  29938  3dim2  29950  llnle  30000  llncmp  30004  lplnle  30022  lplnnle2at  30023  llncvrlpln2  30039  llncvrlpln  30040  lplncmp  30044  lplnexllnN  30046  lvolnle3at  30064  lplncvrlvol2  30097  lplncvrlvol  30098  lvolcmp  30099  pointpsubN  30233  pclfinN  30382  pclfinclN  30432  osumcllem11N  30448  pexmidlem4N  30455  lhprelat3N  30522  cdleme17d3  30978  cdlemeg46gfre  31014  cdleme48gfv1  31018  cdleme50trn2  31033  trlord  31051  cdlemg6e  31104  cdlemj3  31305  diaelrnN  31528  diaintclN  31541  dia2dimlem6  31552  cdlemm10N  31601  dibintclN  31650  dihord6apre  31739  dihord5b  31742  dihord5apre  31745  dihglblem5apreN  31774  dihglblem2N  31777  dihglblem3N  31778  dihglbcpreN  31783  dihintcl  31827  lclkrlem2y  32014  lcfrvalsnN  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator