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

Theorem rexlimdva 2836
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
rexlimdva  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ex 425 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2835 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1727   E.wrex 2712
This theorem is referenced by:  rexlimdvaa  2837  rexlimivv  2841  rexlimdvv  2842  ralxfrd  4766  foco2  5918  elunirnALT  6029  f1elima  6038  tfrlem9a  6676  seqomlem2  6737  oawordexr  6828  odi  6851  oelimcl  6872  nnawordex  6909  nnaordex  6910  oaabs  6916  oaabs2  6917  omabs  6919  ectocld  7000  onfin  7326  dif1enOLD  7369  dif1en  7370  isfinite2  7394  isfiniteg  7396  fofinf1o  7416  elfiun  7464  suplub2  7495  supisoex  7505  ordtypelem9  7524  ordtypelem10  7525  brwdom2  7570  brwdom3  7579  rankr1ai  7753  fodomfi2  7972  infpwfien  7974  dfac12r  8057  ackbij1  8149  cff1  8169  fin23lem21  8250  isf32lem2  8265  fin1a2lem11  8321  fin1a2lem13  8323  ficard  8471  pwcfsdom  8489  gchina  8605  eltsk2g  8657  tskr1om2  8674  rankcf  8683  inatsk  8684  tskuni  8689  nqereu  8837  ltexnq  8883  1idpr  8937  suplem1pr  8960  supsrlem  9017  axpre-sup  9075  1re  9121  supmul1  10004  supmul  10007  suprzcl2  10597  qmulz  10608  qbtwnre  10816  ioo0  10972  ico0  10993  ioc0  10994  icc0  10995  fsequb  11345  hashdom  11684  shftlem  11914  rexuzre  12187  rexico  12188  caubnd  12193  limsupbnd1  12307  limsupbnd2  12308  rlim2lt  12322  rlim3  12323  lo1bdd2  12349  lo1bddrp  12350  o1lo1  12362  climuni  12377  climshftlem  12399  o1co  12411  rlimcn1  12413  climcn1  12416  o1rlimmul  12443  lo1le  12476  rlimno1  12478  isercoll  12492  caurcvg2  12502  serf0  12505  summolem2  12541  zsum  12543  fsum2dlem  12585  geomulcvg  12684  mertenslem2  12693  dvds1lem  12892  odd2np1lem  12938  odd2np1  12939  dvdssqim  13084  coprmdvds2  13134  isprm5  13143  rpexp  13151  pythagtriplem1  13221  iserodd  13240  pc2dvds  13283  prmpwdvds  13303  1arith  13326  4sqlem11  13354  vdwapun  13373  vdwlem2  13381  vdwlem6  13385  vdwlem8  13387  vdwlem10  13389  vdwnnlem1  13394  vdwnnlem3  13396  0ram  13419  ramub1lem2  13426  ramcl  13428  firest  13691  imasvscafn  13793  ffthiso  14157  imasmnd2  14763  imasgrp2  14964  issubg4  14992  gaorber  15116  orbsta  15121  odmulg  15223  odbezout  15225  gexdvdsi  15248  sylow1lem3  15265  odcau  15269  sylow2alem1  15282  sylow3lem6  15297  lsmelvalm  15316  efgrelexlemb  15413  efgredeu  15415  cyggeninv  15524  cygabl  15531  cygctb  15532  cyggexb  15539  dprdssv  15605  dprddisj2  15628  ablfacrplem  15654  pgpfac1lem2  15664  pgpfac1lem5  15668  ablfac2  15678  imasrng  15756  dvdsrcl2  15786  dvdsrmul1  15789  lss1d  16070  lssats2  16107  lspsn  16109  lmhmima  16154  lspsneleq  16218  lpiss  16352  dvdsrz  16798  zlpirlem1  16799  znunit  16875  znrrg  16877  cygznlem3  16881  frgpcyg  16885  tgcl  17065  clsval2  17145  neindisj  17212  innei  17220  restcld  17267  restcldr  17269  ordtrest2lem  17298  cnprest  17384  lmss  17393  lmcls  17397  lmcnp  17399  isnrm3  17454  isreg2  17472  cmpcovf  17485  cncmp  17486  cmpsub  17494  hauscmplem  17500  1stcrest  17547  2ndcrest  17548  2ndcomap  17552  dis2ndc  17554  1stccnp  17556  restnlly  17576  cldllycmp  17589  lly1stc  17590  txcnpi  17671  pthaus  17701  txtube  17703  txcmplem1  17704  txcmplem2  17705  txlm  17711  xkohaus  17716  xkococnlem  17722  xkococn  17723  kqfvima  17793  kqreglem1  17804  isfild  17921  fgcl  17941  filuni  17948  isufil2  17971  ufileu  17982  uffix  17984  rnelfm  18016  fmfnfmlem2  18018  fmfnfmlem4  18020  fmfnfm  18021  fmco  18024  fclsopn  18077  ufilcmp  18095  cnpfcf  18104  alexsublem  18106  alexsubALT  18113  cldsubg  18171  ghmcnp  18175  divstgpopn  18180  tsmsgsum  18199  tsmsres  18204  tsmsxplem1  18213  tsmsxp  18215  isucn2  18340  ucnprima  18343  imasdsf1olem  18434  blssps  18485  blss  18486  blssexps  18487  blssex  18488  mopni3  18555  blcld  18566  metrest  18585  metcnp3  18601  qdensere  18835  reperflem  18880  icccmplem3  18886  opnreen  18893  xrge0tsms  18896  mulc1cncf  18966  cncfco  18968  cnheibor  19011  bndth  19014  lebnumlem3  19019  xlebnum  19021  lebnumii  19022  nmoleub2lem3  19154  nmhmcn  19159  cfil3i  19253  cmetcaulem  19272  cfilres  19280  bcthlem4  19311  bcthlem5  19312  ivthlem2  19380  ivthlem3  19381  ivthicc  19386  cniccbdd  19389  ovolunlem1  19424  ovoliunlem2  19430  ovolshftlem2  19437  ovolicc2lem4  19447  ovolicc2  19449  iundisj  19473  iunmbl2  19482  dyadmax  19521  opnmbllem  19524  subopnmbl  19527  volivth  19530  vitalilem2  19532  ismbf3d  19575  mbfimaopn2  19578  mbfaddlem  19581  i1fmullem  19615  mbfi1fseqlem4  19639  ellimc3  19797  dvlip  19908  dvlip2  19910  c1liplem1  19911  dvgt0lem1  19917  dvivthlem2  19924  dvne0  19926  lhop1lem  19928  lhop2  19930  lhop  19931  mpfind  19996  mpfpf1  20002  pf1mpf  20003  tdeglem4  20014  mdegnn0cl  20025  ply1divex  20090  dvdsq1p  20114  ig1peu  20125  elply2  20146  plypf1  20162  plydivlem4  20244  plydivex  20245  elqaa  20270  aalioulem3  20282  aalioulem5  20284  aaliou  20286  ulmshftlem  20336  ulmuni  20339  ulmcau  20342  ulmss  20344  ulmbdd  20345  ulmcn  20346  radcnvlt1  20365  eflogeq  20527  efopn  20580  cxpeq  20672  angpieqvd  20703  dcubic  20717  xrlimcnp  20838  cxploglim  20847  ftalem2  20887  ftalem7  20892  isppw2  20929  dchrptlem1  21079  dchrptlem3  21081  dchrpt  21082  dchrsum2  21083  lgsdchrval  21162  lgsdchr  21163  lgsquadlem1  21169  dchrisumlem3  21216  dchrisum0fno1  21236  pntlem3  21334  pntleml  21336  ostth3  21363  usgranloop  21430  usgrarnedg1  21439  nbgraf1olem5  21486  vdusgra0nedg  21710  usgravd0nedg  21714  eupai  21720  isgrp2d  21854  ghgrplem1  21985  blocnilem  22336  ubthlem1  22403  ubthlem3  22405  htthlem  22451  shsel3  22848  omlsii  22936  spansncol  23101  nmopun  23548  nmcexi  23560  riesz1  23599  elpjrn  23724  cvcon3  23818  chcv1  23889  atcvatlem  23919  chirredi  23928  iundisjfi  24183  xrge0tsmsd  24254  lmxrge0  24368  indf1ofs  24454  esumcst  24486  esumfsup  24491  esumpcvgval  24499  esumcvg  24507  measdivcstOLD  24609  dstfrvunirn  24763  erdszelem8  24915  erdszelem11  24918  erdsze2lem2  24921  conpcon  24953  sconpi1  24957  cvmsss2  24992  cvmfolem  24997  cvmliftmolem2  25000  cvmliftlem15  25016  cvmlift2lem1  25020  cvmlift3lem4  25040  cvmlift3lem5  25041  ntrivcvg  25256  zprod  25294  fprod2dlem  25335  dvdspw  25400  br8  25410  br6  25411  br4  25412  trpredtr  25539  frrlem5e  25621  brcgr  25870  brbtwn2  25875  axbtwnid  25909  axcontlem2  25935  axcontlem7  25940  cgrtriv  25967  btwntriv2  25977  btwncomim  25978  btwnswapid  25982  btwnintr  25984  btwnexch3  25985  btwnouttr2  25987  ifscgr  26009  cgrxfr  26020  btwnxfr  26021  btwnconn3  26068  segcon2  26070  brsegle  26073  brsegle2  26074  seglecgr12im  26075  broutsideof3  26091  linethru  26118  elhf2  26147  supaddc  26269  supadd  26270  heicant  26277  opnmbllem0  26278  ismblfin  26283  itg2addnclem  26294  itg2addnclem3  26296  itg2gt0cn  26298  bddiblnc  26313  ftc1anclem5  26322  ftc2nc  26327  opnregcld  26371  cldregopn  26372  locfincmp  26422  neibastop2lem  26427  filbcmb  26480  sdclem1  26485  fdc  26487  fdc1  26488  incsequz  26490  caushft  26505  istotbnd3  26518  sstotbnd3  26523  isbnd3  26531  equivbnd  26537  cntotbnd  26543  heibor1lem  26556  heibor1  26557  bfplem2  26570  divrngidl  26676  prnc  26715  prtlem10  26752  elrfi  26786  isnacs3  26802  eldiophb  26853  diophrw  26855  eldioph2b  26859  diophin  26869  eldiophss  26871  diophrex  26872  rexrabdioph  26892  eldioph4b  26910  diophren  26912  rencldnfilem  26919  irrapxlem4  26926  irrapxlem6  26928  pellex  26936  pell1234qrdich  26962  pellfundex  26987  pellfund14b  27000  jm2.26a  27109  jm2.27  27117  lsmfgcl  27187  kercvrlsm  27196  lmhmfgima  27197  lindfrn  27306  islinds4  27320  lpirlnr  27336  hbtlem2  27343  hbtlem4  27345  hbtlem6  27348  mpaaeu  27370  rngunsnply  27393  psgnghm  27452  stoweidlem28  27791  stoweidlem57  27820  stoweidlem60  27823  stoweidlem61  27824  otiunsndisj  28105  otiunsndisjX  28106  ralxfrd2  28111  cshwssizelem1a  28337  cshwsiun  28344  cshwssizesame  28346  el2wlkonot  28425  el2spthonot  28426  el2wlkonotot0  28428  2spontn0vne  28443  2pthfrgra  28499  3cyclfrgrarn1  28500  frgraregorufr  28540  frg2wot1  28544  frg2woteq  28547  2spotiundisj  28549  usg2spot2nb  28552  usgreg2spot  28554  2spotmdisj  28555  lshpdisj  29883  cvrcon3b  30173  atnle  30213  hlhgt2  30284  hl0lt1N  30285  hl2at  30300  cvrexchlem  30314  cvratlem  30316  lvolnlelpln  30480  2lplnj  30515  ispsubcl2N  30842  lautcvr  30987  dva1dim  31880  dib1dim  32061  dib1dim2  32064  diclspsn  32090  dih1dimatlem  32225  dihlatat  32233  dihatexv  32234  dihatexv2  32235  dihjat2  32327  lcfrlem9  32446  lcfrlem16  32454  mapdrvallem2  32541  mapd1o  32544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-11 1763
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2716  df-rex 2717
  Copyright terms: Public domain W3C validator