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

Theorem rexlimdva 2790
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 424 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2789 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  rexlimdvaa  2791  rexlimivv  2795  rexlimdvv  2796  ralxfrd  4696  foco2  5848  elunirnALT  5959  f1elima  5968  tfrlem9a  6606  seqomlem2  6667  oawordexr  6758  odi  6781  oelimcl  6802  nnawordex  6839  nnaordex  6840  oaabs  6846  oaabs2  6847  omabs  6849  ectocld  6930  onfin  7256  dif1enOLD  7299  dif1en  7300  isfinite2  7324  isfiniteg  7326  fofinf1o  7346  elfiun  7393  suplub2  7422  supisoex  7432  ordtypelem9  7451  ordtypelem10  7452  brwdom2  7497  brwdom3  7506  rankr1ai  7680  fodomfi2  7897  infpwfien  7899  dfac12r  7982  ackbij1  8074  cff1  8094  fin23lem21  8175  isf32lem2  8190  fin1a2lem11  8246  fin1a2lem13  8248  ficard  8396  pwcfsdom  8414  gchina  8530  eltsk2g  8582  tskr1om2  8599  rankcf  8608  inatsk  8609  tskuni  8614  nqereu  8762  ltexnq  8808  1idpr  8862  suplem1pr  8885  supsrlem  8942  axpre-sup  9000  1re  9046  supmul1  9929  supmul  9932  suprzcl2  10522  qmulz  10533  qbtwnre  10741  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  fsequb  11269  hashdom  11608  shftlem  11838  rexuzre  12111  rexico  12112  caubnd  12117  limsupbnd1  12231  limsupbnd2  12232  rlim2lt  12246  rlim3  12247  lo1bdd2  12273  lo1bddrp  12274  o1lo1  12286  climuni  12301  climshftlem  12323  o1co  12335  rlimcn1  12337  climcn1  12340  o1rlimmul  12367  lo1le  12400  rlimno1  12402  isercoll  12416  caurcvg2  12426  serf0  12429  summolem2  12465  zsum  12467  fsum2dlem  12509  geomulcvg  12608  mertenslem2  12617  dvds1lem  12816  odd2np1lem  12862  odd2np1  12863  dvdssqim  13008  coprmdvds2  13058  isprm5  13067  rpexp  13075  pythagtriplem1  13145  iserodd  13164  pc2dvds  13207  prmpwdvds  13227  1arith  13250  4sqlem11  13278  vdwapun  13297  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  vdwlem10  13313  vdwnnlem1  13318  vdwnnlem3  13320  0ram  13343  ramub1lem2  13350  ramcl  13352  firest  13615  imasvscafn  13717  ffthiso  14081  imasmnd2  14687  imasgrp2  14888  issubg4  14916  gaorber  15040  orbsta  15045  odmulg  15147  odbezout  15149  gexdvdsi  15172  sylow1lem3  15189  odcau  15193  sylow2alem1  15206  sylow3lem6  15221  lsmelvalm  15240  efgrelexlemb  15337  efgredeu  15339  cyggeninv  15448  cygabl  15455  cygctb  15456  cyggexb  15463  dprdssv  15529  dprddisj2  15552  ablfacrplem  15578  pgpfac1lem2  15588  pgpfac1lem5  15592  ablfac2  15602  imasrng  15680  dvdsrcl2  15710  dvdsrmul1  15713  lss1d  15994  lssats2  16031  lspsn  16033  lmhmima  16078  lspsneleq  16142  lpiss  16276  dvdsrz  16722  zlpirlem1  16723  znunit  16799  znrrg  16801  cygznlem3  16805  frgpcyg  16809  tgcl  16989  clsval2  17069  neindisj  17136  innei  17144  restcld  17190  restcldr  17192  ordtrest2lem  17221  cnprest  17307  lmss  17316  lmcls  17320  lmcnp  17322  isnrm3  17377  isreg2  17395  cmpcovf  17408  cncmp  17409  cmpsub  17417  hauscmplem  17423  1stcrest  17469  2ndcrest  17470  2ndcomap  17474  dis2ndc  17476  1stccnp  17478  restnlly  17498  cldllycmp  17511  lly1stc  17512  txcnpi  17593  pthaus  17623  txtube  17625  txcmplem1  17626  txcmplem2  17627  txlm  17633  xkohaus  17638  xkococnlem  17644  xkococn  17645  kqfvima  17715  kqreglem1  17726  isfild  17843  fgcl  17863  filuni  17870  isufil2  17893  ufileu  17904  uffix  17906  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  fmco  17946  fclsopn  17999  ufilcmp  18017  cnpfcf  18026  alexsublem  18028  alexsubALT  18035  cldsubg  18093  ghmcnp  18097  divstgpopn  18102  tsmsgsum  18121  tsmsres  18126  tsmsxplem1  18135  tsmsxp  18137  isucn2  18262  ucnprima  18265  imasdsf1olem  18356  blssps  18407  blss  18408  blssexps  18409  blssex  18410  mopni3  18477  blcld  18488  metrest  18507  metcnp3  18523  qdensere  18757  reperflem  18802  icccmplem3  18808  opnreen  18815  xrge0tsms  18818  mulc1cncf  18888  cncfco  18890  cnheibor  18933  bndth  18936  lebnumlem3  18941  xlebnum  18943  lebnumii  18944  nmoleub2lem3  19076  nmhmcn  19081  cfil3i  19175  cmetcaulem  19194  cfilres  19202  bcthlem4  19233  bcthlem5  19234  ivthlem2  19302  ivthlem3  19303  ivthicc  19308  cniccbdd  19311  ovolunlem1  19346  ovoliunlem2  19352  ovolshftlem2  19359  ovolicc2lem4  19369  ovolicc2  19371  iundisj  19395  iunmbl2  19404  dyadmax  19443  opnmbllem  19446  subopnmbl  19449  volivth  19452  vitalilem2  19454  ismbf3d  19499  mbfimaopn2  19502  mbfaddlem  19505  i1fmullem  19539  mbfi1fseqlem4  19563  ellimc3  19719  dvlip  19830  dvlip2  19832  c1liplem1  19833  dvgt0lem1  19839  dvivthlem2  19846  dvne0  19848  lhop1lem  19850  lhop2  19852  lhop  19853  mpfind  19918  mpfpf1  19924  pf1mpf  19925  tdeglem4  19936  mdegnn0cl  19947  ply1divex  20012  dvdsq1p  20036  ig1peu  20047  elply2  20068  plypf1  20084  plydivlem4  20166  plydivex  20167  elqaa  20192  aalioulem3  20204  aalioulem5  20206  aaliou  20208  ulmshftlem  20258  ulmuni  20261  ulmcau  20264  ulmss  20266  ulmbdd  20267  ulmcn  20268  radcnvlt1  20287  eflogeq  20449  efopn  20502  cxpeq  20594  angpieqvd  20625  dcubic  20639  xrlimcnp  20760  cxploglim  20769  ftalem2  20809  ftalem7  20814  isppw2  20851  dchrptlem1  21001  dchrptlem3  21003  dchrpt  21004  dchrsum2  21005  lgsdchrval  21084  lgsdchr  21085  lgsquadlem1  21091  dchrisumlem3  21138  dchrisum0fno1  21158  pntlem3  21256  pntleml  21258  ostth3  21285  usgranloop  21352  usgrarnedg1  21361  nbgraf1olem5  21408  vdusgra0nedg  21632  usgravd0nedg  21636  eupai  21642  isgrp2d  21776  ghgrplem1  21907  blocnilem  22258  ubthlem1  22325  ubthlem3  22327  htthlem  22373  shsel3  22770  omlsii  22858  spansncol  23023  nmopun  23470  nmcexi  23482  riesz1  23521  elpjrn  23646  cvcon3  23740  chcv1  23811  atcvatlem  23841  chirredi  23850  iundisjfi  24105  xrge0tsmsd  24176  lmxrge0  24290  indf1ofs  24376  esumcst  24408  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  measdivcstOLD  24531  dstfrvunirn  24685  erdszelem8  24837  erdszelem11  24840  erdsze2lem2  24843  conpcon  24875  sconpi1  24879  cvmsss2  24914  cvmfolem  24919  cvmliftmolem2  24922  cvmliftlem15  24938  cvmlift2lem1  24942  cvmlift3lem4  24962  cvmlift3lem5  24963  ntrivcvg  25178  zprod  25216  fprod2dlem  25257  dvdspw  25317  br8  25327  br6  25328  br4  25329  trpredtr  25447  frrlem5e  25503  brcgr  25743  brbtwn2  25748  axbtwnid  25782  axcontlem2  25808  axcontlem7  25813  cgrtriv  25840  btwntriv2  25850  btwncomim  25851  btwnswapid  25855  btwnintr  25857  btwnexch3  25858  btwnouttr2  25860  ifscgr  25882  cgrxfr  25893  btwnxfr  25894  btwnconn3  25941  segcon2  25943  brsegle  25946  brsegle2  25947  seglecgr12im  25948  broutsideof3  25964  linethru  25991  elhf2  26020  supaddc  26137  supadd  26138  mblfinlem  26143  ismblfin  26146  itg2addnclem  26155  itg2addnclem3  26157  itg2gt0cn  26159  bddiblnc  26174  opnregcld  26223  cldregopn  26224  locfincmp  26274  neibastop2lem  26279  filbcmb  26332  sdclem1  26337  fdc  26339  fdc1  26340  incsequz  26342  caushft  26357  istotbnd3  26370  sstotbnd3  26375  isbnd3  26383  equivbnd  26389  cntotbnd  26395  heibor1lem  26408  heibor1  26409  bfplem2  26422  divrngidl  26528  prnc  26567  prtlem10  26604  elrfi  26638  isnacs3  26654  eldiophb  26705  diophrw  26707  eldioph2b  26711  diophin  26721  eldiophss  26723  diophrex  26724  rexrabdioph  26744  eldioph4b  26762  diophren  26764  rencldnfilem  26771  irrapxlem4  26778  irrapxlem6  26780  pellex  26788  pell1234qrdich  26814  pellfundex  26839  pellfund14b  26852  jm2.26a  26961  jm2.27  26969  lsmfgcl  27040  kercvrlsm  27049  lmhmfgima  27050  lindfrn  27159  islinds4  27173  lpirlnr  27189  hbtlem2  27196  hbtlem4  27198  hbtlem6  27201  mpaaeu  27223  rngunsnply  27246  psgnghm  27305  stoweidlem28  27644  stoweidlem57  27673  stoweidlem60  27676  stoweidlem61  27677  otiunsndisj  27954  otiunsndisjX  27955  el2wlkonot  28066  el2spthonot  28067  el2wlkonotot0  28069  2spontn0vne  28084  2pthfrgra  28115  3cyclfrgrarn1  28116  frgraregorufr  28156  frg2wot1  28160  frg2woteq  28163  2spotiundisj  28165  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  lshpdisj  29470  cvrcon3b  29760  atnle  29800  hlhgt2  29871  hl0lt1N  29872  hl2at  29887  cvrexchlem  29901  cvratlem  29903  lvolnlelpln  30067  2lplnj  30102  ispsubcl2N  30429  lautcvr  30574  dva1dim  31467  dib1dim  31648  dib1dim2  31651  diclspsn  31677  dih1dimatlem  31812  dihlatat  31820  dihatexv  31821  dihatexv2  31822  dihjat2  31914  lcfrlem9  32033  lcfrlem16  32041  mapdrvallem2  32128  mapd1o  32131
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