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

Theorem rexlimdv 2742
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 1619 . 2  |-  F/ x ph
2 nfv 1619 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2740 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   E.wrex 2620
This theorem is referenced by:  rexlimdva  2743  rexlimdv3a  2745  rexlimdvw  2746  rexlimdvv  2749  trintss  4210  tz7.7  4500  elpwunsn  4650  ssorduni  4659  onint  4668  limuni3  4725  funcnvuni  5399  dffo3  5758  isofrlem  5924  weniso  5939  frxp  6312  smoiun  6465  tfrlem9  6488  oaordex  6643  oalimcl  6645  oaass  6646  omlimcl  6663  fisucdomOLD  7154  findcard3  7190  frfi  7192  unblem1  7199  marypha1lem  7276  ordiso2  7320  inf3lem3  7421  noinfepOLD  7451  r1sdom  7536  tz9.12lem3  7551  karden  7655  infxpenlem  7731  cardaleph  7806  cardinfima  7814  iunfictbso  7831  dfac5  7845  cfflb  7975  cfcoflem  7988  coftr  7989  cfcof  7990  fin23lem11  8033  fin23lem30  8058  fin1a2lem13  8128  axdc3lem2  8167  konigthlem  8280  alephval2  8284  pwcfsdom  8295  fpwwe2lem12  8353  tskuni  8495  grur1  8532  axgroth6  8540  inaprc  8548  nqereu  8643  genpnmax  8721  prlem934  8747  ltaddpr  8748  ltexprlem7  8756  reclem3pr  8763  recexsrlem  8815  mulgt0sr  8817  recexsr  8819  axrrecex  8875  axpre-sup  8881  00id  9077  mul02lem1  9078  addid1  9082  addid2  9085  recex  9490  receu  9503  zdiv  10174  btwnz  10206  lbzbi  10398  qbtwnre  10618  caubnd  11938  caucvgb  12249  dvdsval2  12631  divalglem9  12697  unbenlem  13052  firest  13436  isacs3lem  14368  imasmnd2  14508  imasgrp2  14709  pgpfi  15015  sylow2blem3  15032  imasrng  15501  lspsneq  15974  lspdisj  15977  drngnidl  16080  unitg  16811  tgcl  16813  fctop  16847  cctop  16849  elcls  16916  elcls3  16926  restcls  17017  restntr  17018  subbascn  17090  cnpnei  17099  cmpsublem  17232  cmpsub  17233  2ndc1stc  17283  2ndcctbss  17287  nllyidm  17321  ptpjopn  17412  fbfinnfr  17638  filin  17651  isfil2  17653  infil  17660  fbasfip  17665  fgss2  17671  fgfil  17672  fgcl  17675  fgabs  17676  fbasrn  17681  elfm2  17745  elfm3  17747  rnelfmlem  17749  rnelfm  17750  fmfnfmlem2  17752  fmfnfmlem4  17754  fmco  17758  flffbas  17792  cnpflf2  17797  fclscf  17822  alexsubALTlem2  17844  alexsubALTlem3  17845  alexsubALTlem4  17846  alexsubALT  17847  neibl  18149  met2ndc  18171  metcnp3  18188  icccmplem2  18431  xrge0tsms  18442  fgcfil  18801  volfiniun  19008  dyadmax  19057  dyadmbllem  19058  c1liplem1  19447  dgrlem  19715  aaliou3lem8  19829  aaliou3lem9  19834  lpni  20958  grpoidinvlem3  20985  grpoidinvlem4  20986  grporcan  21000  grpoinvf  21019  nmosetre  21456  omlsii  22096  spansncol  22261  spansneleq  22263  spansnss  22264  normcan  22269  spanunsni  22272  h1datomi  22274  chscllem3  22332  nmopsetretALT  22557  nmfnsetre  22571  branmfn  22799  cnvbraval  22804  opsqrlem1  22834  superpos  23048  chjatom  23051  cvbr4i  23061  atomli  23076  xreceu  23372  xrge0tsmsd  23415  esumcst  23721  dstfrvunirn  23981  dfon2lem6  24702  trpredrec  24799  nodenselem5  24897  nobndlem6  24909  brbtwn2  25092  colinearalg  25097  axcontlem10  25160  colineardim1  25243  btwnconn1lem13  25281  outsidele  25314  finminlem  25555  nn0prpwlem  25562  reftr  25613  comppfsc  25631  neibastop2lem  25633  neibastop2  25634  fgmin  25643  tailfb  25650  heiborlem8  25865  heiborlem10  25867  unichnidl  25979  prtlem15  26066  isnacs3  26108  acongrep  26390  jm2.26  26418  jm2.27b  26422  fnwe2lem2  26471  lnrfg  26646  hbtlem5  26655  pmtrfrn  26723  stoweidlem27  27099  stoweidlem28  27100  stoweidlem52  27124  stoweidlem57  27129  stoweidlem59  27131  stoweidlem60  27132  stoweidlem61  27133  stoweidlem62  27134  eldmrexrnb  27430  lshpcmp  29247  lsatn0  29258  lsatcmp  29262  lsmsat  29267  lsatcv0  29290  l1cvpat  29313  eqlkr  29358  lshpkrlem1  29369  lshpkrlem6  29374  lfl1dim  29380  lfl1dim2N  29381  lkrss2N  29428  cvlcvr1  29598  athgt  29714  3dim2  29726  llnle  29776  llncmp  29780  llnmlplnN  29797  lplnle  29798  lplnnle2at  29799  llncvrlpln2  29815  llncvrlpln  29816  lplncmp  29820  lplnexllnN  29822  lvolnle3at  29840  lplncvrlvol2  29873  lplncvrlvol  29874  lvolcmp  29875  pointpsubN  30009  cdlemb  30052  paddasslem10  30087  pclfinN  30158  pclfinclN  30208  osumcllem11N  30224  pexmidlem4N  30231  pexmidlem8N  30235  lhprelat3N  30298  trlcnv  30423  trlator0  30429  trlid0  30434  trlnidatb  30435  cdlemd4  30459  cdleme17d3  30754  cdlemeg46gfre  30790  cdleme48gfv1  30794  cdleme50trn2  30809  trlord  30827  cdlemg5  30863  cdlemg6e  30880  trlco  30985  cdlemj3  31081  tendo0mul  31084  tendo0mulr  31085  tendoconid  31087  erngdv  31251  erngdv-rN  31259  diaelrnN  31304  diaintclN  31317  dia2dimlem6  31328  cdlemm10N  31377  dibintclN  31426  dihord6apre  31515  dihord5b  31518  dihord5apre  31521  dihmeetlem1N  31549  dihglblem5apreN  31550  dihglblem2N  31553  dihglblem3N  31554  dihglbcpreN  31559  dihatlat  31593  dihintcl  31603  lclkrlem2y  31790  lcfrvalsnN  31800  hgmaprnlem5N  32162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2624  df-rex 2625
  Copyright terms: Public domain W3C validator