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

Theorem rexlimdva 2669
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 2668 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685   E.wrex 2546
This theorem is referenced by:  rexlimdvaa  2670  rexlimivv  2674  rexlimdvv  2675  ralxfrd  4548  foco2  5642  elunirnALT  5741  f1elima  5749  grprinvlem  6020  grpridd  6022  tfrlem9a  6398  seqomlem2  6459  oawordexr  6550  odi  6573  oelimcl  6594  nnawordex  6631  nnaordex  6632  oaabs  6638  oaabs2  6639  omabs  6641  ectocld  6722  onfin  7047  dif1enOLD  7086  dif1en  7087  isfinite2  7111  isfiniteg  7113  fofinf1o  7133  fiin  7171  elfiun  7179  suplub2  7208  supisoex  7218  ordtypelem9  7237  ordtypelem10  7238  wemaplem3  7259  brwdom2  7283  brwdom3  7292  cantnflt  7369  oemapvali  7382  cantnflem4  7390  r1pwss  7452  rankr1ai  7466  infxpenc2lem1  7642  fseqenlem2  7648  fodomfi2  7683  infpwfien  7685  dfac12r  7768  ackbij1  7860  cff1  7880  fin23lem26  7947  fin23lem21  7961  isf32lem2  7976  fin1a2lem11  8032  fin1a2lem13  8034  ficard  8183  pwcfsdom  8201  fpwwe2  8261  pwfseqlem3  8278  gchina  8317  r1wunlim  8355  wunex2  8356  eltsk2g  8369  tskr1om2  8386  inttsk  8392  rankcf  8395  inatsk  8396  tskuni  8401  nqereu  8549  ltexnq  8595  1idpr  8649  suplem1pr  8672  supsrlem  8729  axpre-sup  8787  1re  8833  addcan  8992  addcan2  8993  negeu  9038  mulcand  9397  supmul1  9715  supmul  9718  suprzcl  10087  zsupss  10303  suprzcl2  10304  uzwo3  10307  qmulz  10315  qbtwnre  10521  xralrple  10527  ioo0  10676  ico0  10697  ioc0  10698  icc0  10699  fsequb  11032  expmulnbnd  11228  hashdom  11356  shftlem  11558  rexanuz  11824  rexuzre  11831  rexico  11832  caubnd  11837  limsupval2  11949  limsupgre  11950  limsupbnd1  11951  limsupbnd2  11952  rlim2lt  11966  rlim3  11967  lo1bdd2  11993  lo1bddrp  11994  o1lo1  12006  rlimclim1  12014  climuni  12021  climshftlem  12043  o1co  12055  rlimcn1  12057  climcn1  12060  o1rlimmul  12087  lo1le  12120  rlimno1  12122  isercoll  12136  caurcvg2  12145  serf0  12148  summolem2  12184  zsum  12186  fsumcvg3  12197  fsum2dlem  12228  fsumiun  12274  geomulcvg  12327  mertenslem2  12336  rpnnen2  12499  dvds1lem  12535  odd2np1lem  12581  odd2np1  12582  oexpneg  12585  bitsfi  12623  dvdssqim  12727  prmind2  12764  coprmdvds2  12777  isprm5  12786  rpexp  12794  pythagtriplem1  12864  iserodd  12883  pc2dvds  12926  pcprmpw2  12929  prmpwdvds  12946  pockthg  12948  prmreclem5  12962  1arith  12969  4sqlem11  12997  vdwapun  13016  vdwlem2  13024  vdwlem6  13028  vdwlem8  13030  vdwlem10  13032  vdwnnlem1  13037  vdwnnlem3  13039  0ram  13062  ramub1lem2  13069  ramcl  13071  firest  13332  imasvscafn  13434  ffthiso  13798  drsdirfi  14067  imasmnd2  14404  grprcan  14510  imasgrp2  14605  issubg4  14633  gaorber  14757  orbsta  14762  odmulg  14864  odbezout  14866  gexdvdsi  14889  sylow1lem3  14906  sylow1  14909  odcau  14910  pgpfi  14911  sylow2alem1  14923  slwhash  14930  sylow3lem2  14934  sylow3lem6  14938  lsmelvalm  14957  pj1id  15003  efgsfo  15043  efgredlemc  15049  efgrelexlemb  15054  efgredeu  15056  cyggeninv  15165  cygabl  15172  cygctb  15173  lt6abl  15176  ghmcyg  15177  cyggexb  15180  dprdssv  15246  dmdprdsplitlem  15267  dprddisj2  15269  dpjidcl  15288  ablfacrplem  15295  pgpfac1lem2  15305  pgpfac1lem4  15308  pgpfac1lem5  15309  pgpfaclem2  15312  pgpfaclem3  15313  ablfac2  15319  imasrng  15397  dvdsrcl2  15427  dvdsrmul1  15430  unitgrp  15444  irredrmul  15484  lss1d  15715  lssats2  15752  lspsn  15754  lmhmima  15799  lspsneleq  15863  lspsolv  15891  lpiss  15997  dvdsrz  16435  zlpirlem1  16436  znunit  16512  znrrg  16514  cygznlem3  16518  frgpcyg  16522  tgcl  16702  clsval2  16782  neiint  16836  neindisj  16849  innei  16857  restbas  16884  restcld  16898  restcldr  16900  restopnb  16901  ordtrest2lem  16928  pnfnei  16945  mnfnei  16946  cnpco  16991  cnprest  17012  lmss  17021  lmcls  17025  lmcnp  17027  pnrmopn  17066  haust1  17075  isnrm3  17082  isreg2  17100  ordthauslem  17106  cmpcovf  17113  cncmp  17114  cmpsub  17122  tgcmp  17123  hauscmplem  17128  t1conperf  17157  1stcfb  17166  1stcrest  17174  2ndcrest  17175  2ndcdisj  17177  2ndcomap  17179  dis2ndc  17181  1stccnp  17183  restnlly  17203  islly2  17205  nllyrest  17207  llyidm  17209  nllyidm  17210  hausllycmp  17215  cldllycmp  17216  lly1stc  17217  llycmpkgen2  17240  1stckgenlem  17243  ptbasfi  17271  txcnpi  17297  ptcnp  17311  pthaus  17327  txtube  17329  txcmplem1  17330  txcmplem2  17331  txlm  17337  xkohaus  17342  xkococnlem  17348  xkococn  17349  basqtop  17397  tgqtop  17398  kqfvima  17416  regr1lem  17425  kqreglem1  17427  kqreglem2  17428  kqnrmlem1  17429  kqnrmlem2  17430  reghmph  17479  nrmhmph  17480  qtophmeo  17503  fbssfi  17527  trfbas2  17533  isfild  17548  fgcl  17568  fgabs  17569  neifil  17570  filuni  17575  trfil2  17577  trfg  17581  isufil2  17598  ssufl  17608  ufileu  17609  uffix  17611  rnelfm  17643  fmfnfmlem2  17645  fmfnfmlem4  17647  fmfnfm  17648  fmufil  17649  fmco  17651  ufldom  17652  fclsopn  17704  fclsfnflim  17717  uffclsflim  17721  ufilcmp  17722  cnpfcfi  17730  cnpfcf  17731  alexsublem  17733  alexsubALT  17740  ptcmplem3  17743  ptcmplem4  17744  cldsubg  17788  ghmcnp  17792  divstgpopn  17797  tsmsgsum  17816  tsmsres  17821  tsmsxplem1  17830  tsmsxp  17832  imasdsf1olem  17932  blss  17967  blssex  17968  mopni3  18035  blcld  18046  met1stc  18062  met2ndci  18063  metrest  18065  prdsxmslem2  18070  metcnp3  18081  metcnpi3  18087  qdensere  18274  reperflem  18318  icccmplem1  18322  icccmplem3  18324  opnreen  18331  xrge0tsms  18334  metdseq0  18353  mulc1cncf  18404  cncfco  18406  cnheibor  18448  cnllycmp  18449  bndth  18451  lebnumlem1  18454  lebnumlem3  18456  lebnum  18457  xlebnum  18458  lebnumii  18459  pi1blem  18532  nmoleub2lem3  18591  nmhmcn  18596  cfil3i  18690  iscfil3  18694  cfilfcls  18695  cmetcaulem  18709  iscmet3lem2  18713  cfilres  18717  lmle  18722  cmetss  18735  relcmpcmet  18737  bcthlem4  18744  bcthlem5  18745  pjthlem2  18797  ivthlem2  18807  ivthlem3  18808  ivthicc  18813  cniccbdd  18816  ovolunlem1  18851  ovoliunlem2  18857  ovolshftlem2  18864  ovolscalem2  18868  ovolicc2lem4  18874  ovolicc2lem5  18875  ovolicc2  18876  nulmbl2  18889  iundisj  18900  volsup  18908  iunmbl2  18909  ioombl1  18914  uniioombllem6  18938  uniioombl  18939  dyadmax  18948  dyadmbllem  18949  opnmbllem  18951  subopnmbl  18954  volivth  18957  vitalilem2  18959  ismbf3d  19004  mbfimaopn2  19007  mbfaddlem  19010  mbfinf  19015  i1fmullem  19044  mbfi1fseqlem4  19068  mbfi1fseqlem6  19070  itg2const2  19091  itg2cnlem1  19111  itg2cn  19113  bddmulibl  19188  ellimc3  19224  limcflf  19226  dvlip  19335  dvlip2  19337  c1liplem1  19338  dvgt0lem1  19344  dvivthlem2  19351  dvne0  19353  lhop1lem  19355  lhop2  19357  lhop  19358  dvcnvre  19361  itgsubst  19391  mpfind  19423  mpfpf1  19429  pf1mpf  19430  tdeglem4  19441  mdegnn0cl  19452  ply1divex  19517  dvdsq1p  19541  ig1peu  19552  elply2  19573  plypf1  19589  plydivlem4  19671  plydivex  19672  elqaa  19697  aareccl  19701  aalioulem3  19709  aalioulem5  19711  aaliou  19713  ulmshftlem  19763  ulmcau  19767  ulmss  19769  ulmbdd  19770  ulmcn  19771  ulmdvlem3  19774  iblulm  19778  radcnvlem1  19784  radcnvlt1  19789  abelthlem5  19806  abelthlem8  19810  eflogeq  19950  efopn  20000  cxpeq  20092  angpieqvd  20123  dcubic  20137  xrlimcnp  20258  cxploglim  20267  amgm  20280  ftalem2  20306  ftalem7  20311  fta  20312  isppw2  20348  dchrptlem1  20498  dchrptlem2  20499  dchrptlem3  20500  dchrpt  20501  dchrsum2  20502  sumdchr2  20504  lgsne0  20567  lgsqr  20580  lgsdchrval  20581  lgsdchr  20582  lgsquadlem1  20588  2sqlem11  20609  dchrisumlem3  20635  dchrisum  20636  dchrvmasumif  20647  dchrisum0flb  20654  dchrisum0fno1  20655  rpvmasum2  20656  dchrisum0re  20657  dchrisum0lem3  20663  dchrisum0  20664  dchrmusum  20668  dchrvmasum  20669  chpdifbnd  20699  pntrlog2bnd  20728  pntibndlem3  20736  pntibnd  20737  pntlemi  20748  pntlem3  20753  pntleml  20755  ostth3  20782  ostth  20783  isgrp2d  20895  ghgrplem1  21026  nmobndi  21346  blocnilem  21375  ubthlem1  21442  ubthlem3  21444  htthlem  21490  shsel3  21887  omlsii  21975  spansncol  22140  pjspansn  22149  nmopun  22587  nmcexi  22599  riesz1  22638  elpjrn  22763  cvcon3  22857  chcv1  22928  atcvatlem  22958  chirredi  22967  erdszelem8  23134  erdszelem11  23137  erdsze2lem2  23140  cnpcon  23166  pconcon  23167  conpcon  23171  pconpi1  23173  sconpi1  23175  cnllyscon  23181  cvmsss2  23210  cvmcov2  23211  cvmfolem  23215  cvmliftmolem2  23218  cvmliftlem15  23234  cvmlift2lem1  23238  cvmlift2lem10  23248  cvmliftpht  23254  cvmlift3lem2  23256  cvmlift3lem4  23258  cvmlift3lem5  23259  eupai  23288  sinccvg  23411  dvdspw  23507  br8  23517  br6  23518  br4  23519  trpredtr  23635  frrlem5e  23691  axfelem20  23767  brcgr  23936  brbtwn2  23941  axbtwnid  23975  axcontlem2  24001  axcontlem7  24006  cgrtriv  24033  btwntriv2  24043  btwncomim  24044  btwnswapid  24048  btwnintr  24050  btwnexch3  24051  btwnouttr2  24053  ifscgr  24075  cgrxfr  24086  btwnxfr  24087  btwnconn3  24134  segcon2  24136  brsegle  24139  brsegle2  24140  seglecgr12im  24141  broutsideof3  24157  linethru  24184  elhf2  24213  iscnp4  24963  exopcopn  24972  flfnei2  24977  islimrs3  24981  altretop  25000  vtarsuelt  25295  abhp  25573  opnregcld  25648  cldregopn  25649  locfincmp  25704  comppfsc  25707  neibastop1  25708  neibastop2lem  25709  filbcmb  25832  sdclem1  25853  fdc  25855  fdc1  25856  incsequz  25858  caushft  25877  istotbnd3  25895  sstotbnd2  25898  sstotbnd  25899  sstotbnd3  25900  isbndx  25906  isbnd3  25908  ssbnd  25912  totbndbnd  25913  equivbnd  25914  prdsbnd2  25919  cntotbnd  25920  heibor1lem  25933  heibor1  25934  heiborlem9  25943  heibor  25945  bfplem2  25947  divrngidl  26053  prnc  26092  prtlem10  26133  elrfi  26169  isnacs3  26185  eldiophb  26236  diophrw  26238  eldioph2b  26242  diophin  26252  eldiophss  26254  diophrex  26255  rexrabdioph  26275  eldioph4b  26294  diophren  26296  rencldnfilem  26303  irrapxlem4  26310  irrapxlem6  26312  pellex  26320  pell1234qrdich  26346  pellfundex  26371  pellfund14b  26384  jm2.26a  26493  jm2.27  26501  fnwe2lem2  26548  lsmfgcl  26572  kercvrlsm  26581  lmhmfgima  26582  lmhmfgsplit  26584  lindfrn  26691  islinds4  26705  lpirlnr  26721  hbtlem2  26728  hbtlem4  26730  hbtlem5  26732  hbtlem6  26733  hbt  26734  mpaaeu  26755  rngunsnply  26778  psgnunilem3  26819  psgnghm  26837  lshpdisj  28445  cvrcon3b  28735  atnle  28775  hlhgt2  28846  hl0lt1N  28847  hl2at  28862  cvrexchlem  28876  cvratlem  28878  lvolnlelpln  29042  2lplnj  29077  ispsubcl2N  29404  lautcvr  29549  dva1dim  30442  dib1dim  30623  dib1dim2  30626  diclspsn  30652  dih1dimatlem  30787  dihlatat  30795  dihatexv  30796  dihatexv2  30797  dihjat2  30889  lcfrlem9  31008  lcfrlem16  31016  mapdrvallem2  31103  mapd1o  31106
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533  df-ral 2550  df-rex 2551
  Copyright terms: Public domain W3C validator