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

Theorem rexlimdva 2822
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 2821 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  rexlimdvaa  2823  rexlimivv  2827  rexlimdvv  2828  ralxfrd  4728  foco2  5880  elunirnALT  5991  f1elima  6000  tfrlem9a  6638  seqomlem2  6699  oawordexr  6790  odi  6813  oelimcl  6834  nnawordex  6871  nnaordex  6872  oaabs  6878  oaabs2  6879  omabs  6881  ectocld  6962  onfin  7288  dif1enOLD  7331  dif1en  7332  isfinite2  7356  isfiniteg  7358  fofinf1o  7378  elfiun  7426  suplub2  7455  supisoex  7465  ordtypelem9  7484  ordtypelem10  7485  brwdom2  7530  brwdom3  7539  rankr1ai  7713  fodomfi2  7930  infpwfien  7932  dfac12r  8015  ackbij1  8107  cff1  8127  fin23lem21  8208  isf32lem2  8223  fin1a2lem11  8279  fin1a2lem13  8281  ficard  8429  pwcfsdom  8447  gchina  8563  eltsk2g  8615  tskr1om2  8632  rankcf  8641  inatsk  8642  tskuni  8647  nqereu  8795  ltexnq  8841  1idpr  8895  suplem1pr  8918  supsrlem  8975  axpre-sup  9033  1re  9079  supmul1  9962  supmul  9965  suprzcl2  10555  qmulz  10566  qbtwnre  10774  ioo0  10930  ico0  10951  ioc0  10952  icc0  10953  fsequb  11302  hashdom  11641  shftlem  11871  rexuzre  12144  rexico  12145  caubnd  12150  limsupbnd1  12264  limsupbnd2  12265  rlim2lt  12279  rlim3  12280  lo1bdd2  12306  lo1bddrp  12307  o1lo1  12319  climuni  12334  climshftlem  12356  o1co  12368  rlimcn1  12370  climcn1  12373  o1rlimmul  12400  lo1le  12433  rlimno1  12435  isercoll  12449  caurcvg2  12459  serf0  12462  summolem2  12498  zsum  12500  fsum2dlem  12542  geomulcvg  12641  mertenslem2  12650  dvds1lem  12849  odd2np1lem  12895  odd2np1  12896  dvdssqim  13041  coprmdvds2  13091  isprm5  13100  rpexp  13108  pythagtriplem1  13178  iserodd  13197  pc2dvds  13240  prmpwdvds  13260  1arith  13283  4sqlem11  13311  vdwapun  13330  vdwlem2  13338  vdwlem6  13342  vdwlem8  13344  vdwlem10  13346  vdwnnlem1  13351  vdwnnlem3  13353  0ram  13376  ramub1lem2  13383  ramcl  13385  firest  13648  imasvscafn  13750  ffthiso  14114  imasmnd2  14720  imasgrp2  14921  issubg4  14949  gaorber  15073  orbsta  15078  odmulg  15180  odbezout  15182  gexdvdsi  15205  sylow1lem3  15222  odcau  15226  sylow2alem1  15239  sylow3lem6  15254  lsmelvalm  15273  efgrelexlemb  15370  efgredeu  15372  cyggeninv  15481  cygabl  15488  cygctb  15489  cyggexb  15496  dprdssv  15562  dprddisj2  15585  ablfacrplem  15611  pgpfac1lem2  15621  pgpfac1lem5  15625  ablfac2  15635  imasrng  15713  dvdsrcl2  15743  dvdsrmul1  15746  lss1d  16027  lssats2  16064  lspsn  16066  lmhmima  16111  lspsneleq  16175  lpiss  16309  dvdsrz  16755  zlpirlem1  16756  znunit  16832  znrrg  16834  cygznlem3  16838  frgpcyg  16842  tgcl  17022  clsval2  17102  neindisj  17169  innei  17177  restcld  17224  restcldr  17226  ordtrest2lem  17255  cnprest  17341  lmss  17350  lmcls  17354  lmcnp  17356  isnrm3  17411  isreg2  17429  cmpcovf  17442  cncmp  17443  cmpsub  17451  hauscmplem  17457  1stcrest  17504  2ndcrest  17505  2ndcomap  17509  dis2ndc  17511  1stccnp  17513  restnlly  17533  cldllycmp  17546  lly1stc  17547  txcnpi  17628  pthaus  17658  txtube  17660  txcmplem1  17661  txcmplem2  17662  txlm  17668  xkohaus  17673  xkococnlem  17679  xkococn  17680  kqfvima  17750  kqreglem1  17761  isfild  17878  fgcl  17898  filuni  17905  isufil2  17928  ufileu  17939  uffix  17941  rnelfm  17973  fmfnfmlem2  17975  fmfnfmlem4  17977  fmfnfm  17978  fmco  17981  fclsopn  18034  ufilcmp  18052  cnpfcf  18061  alexsublem  18063  alexsubALT  18070  cldsubg  18128  ghmcnp  18132  divstgpopn  18137  tsmsgsum  18156  tsmsres  18161  tsmsxplem1  18170  tsmsxp  18172  isucn2  18297  ucnprima  18300  imasdsf1olem  18391  blssps  18442  blss  18443  blssexps  18444  blssex  18445  mopni3  18512  blcld  18523  metrest  18542  metcnp3  18558  qdensere  18792  reperflem  18837  icccmplem3  18843  opnreen  18850  xrge0tsms  18853  mulc1cncf  18923  cncfco  18925  cnheibor  18968  bndth  18971  lebnumlem3  18976  xlebnum  18978  lebnumii  18979  nmoleub2lem3  19111  nmhmcn  19116  cfil3i  19210  cmetcaulem  19229  cfilres  19237  bcthlem4  19268  bcthlem5  19269  ivthlem2  19337  ivthlem3  19338  ivthicc  19343  cniccbdd  19346  ovolunlem1  19381  ovoliunlem2  19387  ovolshftlem2  19394  ovolicc2lem4  19404  ovolicc2  19406  iundisj  19430  iunmbl2  19439  dyadmax  19478  opnmbllem  19481  subopnmbl  19484  volivth  19487  vitalilem2  19489  ismbf3d  19534  mbfimaopn2  19537  mbfaddlem  19540  i1fmullem  19574  mbfi1fseqlem4  19598  ellimc3  19754  dvlip  19865  dvlip2  19867  c1liplem1  19868  dvgt0lem1  19874  dvivthlem2  19881  dvne0  19883  lhop1lem  19885  lhop2  19887  lhop  19888  mpfind  19953  mpfpf1  19959  pf1mpf  19960  tdeglem4  19971  mdegnn0cl  19982  ply1divex  20047  dvdsq1p  20071  ig1peu  20082  elply2  20103  plypf1  20119  plydivlem4  20201  plydivex  20202  elqaa  20227  aalioulem3  20239  aalioulem5  20241  aaliou  20243  ulmshftlem  20293  ulmuni  20296  ulmcau  20299  ulmss  20301  ulmbdd  20302  ulmcn  20303  radcnvlt1  20322  eflogeq  20484  efopn  20537  cxpeq  20629  angpieqvd  20660  dcubic  20674  xrlimcnp  20795  cxploglim  20804  ftalem2  20844  ftalem7  20849  isppw2  20886  dchrptlem1  21036  dchrptlem3  21038  dchrpt  21039  dchrsum2  21040  lgsdchrval  21119  lgsdchr  21120  lgsquadlem1  21126  dchrisumlem3  21173  dchrisum0fno1  21193  pntlem3  21291  pntleml  21293  ostth3  21320  usgranloop  21387  usgrarnedg1  21396  nbgraf1olem5  21443  vdusgra0nedg  21667  usgravd0nedg  21671  eupai  21677  isgrp2d  21811  ghgrplem1  21942  blocnilem  22293  ubthlem1  22360  ubthlem3  22362  htthlem  22408  shsel3  22805  omlsii  22893  spansncol  23058  nmopun  23505  nmcexi  23517  riesz1  23556  elpjrn  23681  cvcon3  23775  chcv1  23846  atcvatlem  23876  chirredi  23885  iundisjfi  24140  xrge0tsmsd  24211  lmxrge0  24325  indf1ofs  24411  esumcst  24443  esumfsup  24448  esumpcvgval  24456  esumcvg  24464  measdivcstOLD  24566  dstfrvunirn  24720  erdszelem8  24872  erdszelem11  24875  erdsze2lem2  24878  conpcon  24910  sconpi1  24914  cvmsss2  24949  cvmfolem  24954  cvmliftmolem2  24957  cvmliftlem15  24973  cvmlift2lem1  24977  cvmlift3lem4  24997  cvmlift3lem5  24998  ntrivcvg  25214  zprod  25252  fprod2dlem  25293  dvdspw  25358  br8  25368  br6  25369  br4  25370  trpredtr  25488  frrlem5e  25544  brcgr  25787  brbtwn2  25792  axbtwnid  25826  axcontlem2  25852  axcontlem7  25857  cgrtriv  25884  btwntriv2  25894  btwncomim  25895  btwnswapid  25899  btwnintr  25901  btwnexch3  25902  btwnouttr2  25904  ifscgr  25926  cgrxfr  25937  btwnxfr  25938  btwnconn3  25985  segcon2  25987  brsegle  25990  brsegle2  25991  seglecgr12im  25992  broutsideof3  26008  linethru  26035  elhf2  26064  supaddc  26184  supadd  26185  mblfinlem  26190  ismblfin  26193  itg2addnclem  26202  itg2addnclem3  26204  itg2gt0cn  26206  bddiblnc  26221  opnregcld  26270  cldregopn  26271  locfincmp  26321  neibastop2lem  26326  filbcmb  26379  sdclem1  26384  fdc  26386  fdc1  26387  incsequz  26389  caushft  26404  istotbnd3  26417  sstotbnd3  26422  isbnd3  26430  equivbnd  26436  cntotbnd  26442  heibor1lem  26455  heibor1  26456  bfplem2  26469  divrngidl  26575  prnc  26614  prtlem10  26651  elrfi  26685  isnacs3  26701  eldiophb  26752  diophrw  26754  eldioph2b  26758  diophin  26768  eldiophss  26770  diophrex  26771  rexrabdioph  26791  eldioph4b  26809  diophren  26811  rencldnfilem  26818  irrapxlem4  26825  irrapxlem6  26827  pellex  26835  pell1234qrdich  26861  pellfundex  26886  pellfund14b  26899  jm2.26a  27008  jm2.27  27016  lsmfgcl  27087  kercvrlsm  27096  lmhmfgima  27097  lindfrn  27206  islinds4  27220  lpirlnr  27236  hbtlem2  27243  hbtlem4  27245  hbtlem6  27248  mpaaeu  27270  rngunsnply  27293  psgnghm  27352  stoweidlem28  27691  stoweidlem57  27720  stoweidlem60  27723  stoweidlem61  27724  otiunsndisj  28002  otiunsndisjX  28003  ralxfrd2  28005  shwrdssizelem1a  28165  shwrdssizesame  28171  shwrdsiun  28172  el2wlkonot  28210  el2spthonot  28211  el2wlkonotot0  28213  2spontn0vne  28228  2pthfrgra  28259  3cyclfrgrarn1  28260  frgraregorufr  28300  frg2wot1  28304  frg2woteq  28307  2spotiundisj  28309  usg2spot2nb  28312  usgreg2spot  28314  2spotmdisj  28315  lshpdisj  29624  cvrcon3b  29914  atnle  29954  hlhgt2  30025  hl0lt1N  30026  hl2at  30041  cvrexchlem  30055  cvratlem  30057  lvolnlelpln  30221  2lplnj  30256  ispsubcl2N  30583  lautcvr  30728  dva1dim  31621  dib1dim  31802  dib1dim2  31805  diclspsn  31831  dih1dimatlem  31966  dihlatat  31974  dihatexv  31975  dihatexv2  31976  dihjat2  32068  lcfrlem9  32187  lcfrlem16  32195  mapdrvallem2  32282  mapd1o  32285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator