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

Theorem rexlimdva 2629
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 2628 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2510
This theorem is referenced by:  rexlimdvaa  2630  rexlimivv  2634  rexlimdvv  2635  ralxfrd  4439  foco2  5532  elunirnALT  5631  f1elima  5639  grprinvlem  5910  grpridd  5912  tfrlem9a  6288  seqomlem2  6349  oawordexr  6440  odi  6463  oelimcl  6484  nnawordex  6521  nnaordex  6522  oaabs  6528  oaabs2  6529  omabs  6531  ectocld  6612  onfin  6936  dif1enOLD  6975  dif1en  6976  isfinite2  7000  isfiniteg  7002  fofinf1o  7022  fiin  7059  elfiun  7067  suplub2  7096  supisoex  7106  ordtypelem9  7125  ordtypelem10  7126  wemaplem3  7147  brwdom2  7171  brwdom3  7180  cantnflt  7257  oemapvali  7270  cantnflem4  7278  r1pwss  7340  rankr1ai  7354  infxpenc2lem1  7530  fseqenlem2  7536  fodomfi2  7571  infpwfien  7573  dfac12r  7656  ackbij1  7748  cff1  7768  fin23lem26  7835  fin23lem21  7849  isf32lem2  7864  fin1a2lem11  7920  fin1a2lem13  7922  ficard  8069  pwcfsdom  8085  fpwwe2  8145  pwfseqlem3  8162  gchina  8201  r1wunlim  8239  wunex2  8240  eltsk2g  8253  tskr1om2  8270  inttsk  8276  rankcf  8279  inatsk  8280  tskuni  8285  nqereu  8433  ltexnq  8479  1idpr  8533  suplem1pr  8556  supsrlem  8613  axpre-sup  8671  1re  8717  addcan  8876  addcan2  8877  negeu  8922  mulcand  9281  supmul1  9599  supmul  9602  suprzcl  9970  zsupss  10186  suprzcl2  10187  uzwo3  10190  qmulz  10198  qbtwnre  10404  xralrple  10410  ioo0  10559  ico0  10580  ioc0  10581  icc0  10582  fsequb  10915  expmulnbnd  11111  hashdom  11239  shftlem  11440  rexanuz  11706  rexuzre  11713  rexico  11714  caubnd  11719  limsupval2  11831  limsupgre  11832  limsupbnd1  11833  limsupbnd2  11834  rlim2lt  11848  rlim3  11849  lo1bdd2  11875  lo1bddrp  11876  o1lo1  11888  rlimclim1  11896  climuni  11903  climshftlem  11925  o1co  11937  rlimcn1  11939  climcn1  11942  o1rlimmul  11969  lo1le  12002  rlimno1  12004  isercoll  12018  caurcvg2  12027  serf0  12030  summolem2  12066  zsum  12068  fsumcvg3  12079  fsum2dlem  12110  fsumiun  12156  geomulcvg  12206  mertenslem2  12215  rpnnen2  12378  dvds1lem  12414  odd2np1lem  12460  odd2np1  12461  oexpneg  12464  bitsfi  12502  dvdssqim  12606  prmind2  12643  coprmdvds2  12656  isprm5  12665  rpexp  12673  pythagtriplem1  12743  iserodd  12762  pc2dvds  12805  pcprmpw2  12808  prmpwdvds  12825  pockthg  12827  prmreclem5  12841  1arith  12848  4sqlem11  12876  vdwapun  12895  vdwlem2  12903  vdwlem6  12907  vdwlem8  12909  vdwlem10  12911  vdwnnlem1  12916  vdwnnlem3  12918  0ram  12941  ramub1lem2  12948  ramcl  12950  firest  13211  imasvscafn  13313  ffthiso  13647  drsdirfi  13916  imasmnd2  14244  grprcan  14350  imasgrp2  14445  issubg4  14473  gaorber  14597  orbsta  14602  odmulg  14704  odbezout  14706  gexdvdsi  14729  sylow1lem3  14746  sylow1  14749  odcau  14750  pgpfi  14751  sylow2alem1  14763  slwhash  14770  sylow3lem2  14774  sylow3lem6  14778  lsmelvalm  14797  pj1id  14843  efgsfo  14883  efgredlemc  14889  efgrelexlemb  14894  efgredeu  14896  cyggeninv  15005  cygabl  15012  cygctb  15013  lt6abl  15016  ghmcyg  15017  cyggexb  15020  dprdssv  15086  dmdprdsplitlem  15107  dprddisj2  15109  dpjidcl  15128  ablfacrplem  15135  pgpfac1lem2  15145  pgpfac1lem4  15148  pgpfac1lem5  15149  pgpfaclem2  15152  pgpfaclem3  15153  ablfac2  15159  imasrng  15237  dvdsrcl2  15267  dvdsrmul1  15270  unitgrp  15284  irredrmul  15324  lss1d  15555  lssats2  15592  lspsn  15594  lmhmima  15639  lspsneleq  15703  lspsolv  15731  lpiss  15834  dvdsrz  16272  zlpirlem1  16273  znunit  16349  znrrg  16351  cygznlem3  16355  frgpcyg  16359  tgcl  16539  clsval2  16619  neiint  16673  neindisj  16686  innei  16694  restbas  16721  restcld  16735  restcldr  16737  restopnb  16738  ordtrest2lem  16765  pnfnei  16782  mnfnei  16783  cnpco  16828  cnprest  16849  lmss  16858  lmcls  16862  lmcnp  16864  pnrmopn  16903  haust1  16912  isnrm3  16919  isreg2  16937  ordthauslem  16943  cmpcovf  16950  cncmp  16951  cmpsub  16959  tgcmp  16960  hauscmplem  16965  t1conperf  16994  1stcfb  17003  1stcrest  17011  2ndcrest  17012  2ndcdisj  17014  2ndcomap  17016  dis2ndc  17018  1stccnp  17020  restnlly  17040  islly2  17042  nllyrest  17044  llyidm  17046  nllyidm  17047  hausllycmp  17052  cldllycmp  17053  lly1stc  17054  llycmpkgen2  17077  1stckgenlem  17080  ptbasfi  17108  txcnpi  17134  ptcnp  17148  pthaus  17164  txtube  17166  txcmplem1  17167  txcmplem2  17168  txlm  17174  xkohaus  17179  xkococnlem  17185  xkococn  17186  basqtop  17234  tgqtop  17235  kqfvima  17253  regr1lem  17262  kqreglem1  17264  kqreglem2  17265  kqnrmlem1  17266  kqnrmlem2  17267  reghmph  17316  nrmhmph  17317  qtophmeo  17340  fbssfi  17364  trfbas2  17370  isfild  17385  fgcl  17405  fgabs  17406  neifil  17407  filuni  17412  trfil2  17414  trfg  17418  isufil2  17435  ssufl  17445  ufileu  17446  uffix  17448  rnelfm  17480  fmfnfmlem2  17482  fmfnfmlem4  17484  fmfnfm  17485  fmufil  17486  fmco  17488  ufldom  17489  fclsopn  17541  fclsfnflim  17554  uffclsflim  17558  ufilcmp  17559  cnpfcfi  17567  cnpfcf  17568  alexsublem  17570  alexsubALT  17577  ptcmplem3  17580  ptcmplem4  17581  cldsubg  17625  ghmcnp  17629  divstgpopn  17634  tsmsgsum  17653  tsmsres  17658  tsmsxplem1  17667  tsmsxp  17669  imasdsf1olem  17769  blss  17804  blssex  17805  mopni3  17872  blcld  17883  met1stc  17899  met2ndci  17900  metrest  17902  prdsxmslem2  17907  metcnp3  17918  metcnpi3  17924  qdensere  18111  reperflem  18155  icccmplem1  18159  icccmplem3  18161  opnreen  18168  xrge0tsms  18171  metdseq0  18190  mulc1cncf  18241  cncfco  18243  cnheibor  18285  cnllycmp  18286  bndth  18288  lebnumlem1  18291  lebnumlem3  18293  lebnum  18294  xlebnum  18295  lebnumii  18296  pi1blem  18369  nmoleub2lem3  18428  nmhmcn  18433  cfil3i  18527  iscfil3  18531  cfilfcls  18532  cmetcaulem  18546  iscmet3lem2  18550  cfilres  18554  lmle  18559  cmetss  18572  relcmpcmet  18574  bcthlem4  18581  bcthlem5  18582  pjthlem2  18634  ivthlem2  18644  ivthlem3  18645  ivthicc  18650  cniccbdd  18653  ovolunlem1  18688  ovoliunlem2  18694  ovolshftlem2  18701  ovolscalem2  18705  ovolicc2lem4  18711  ovolicc2lem5  18712  ovolicc2  18713  nulmbl2  18726  iundisj  18737  volsup  18745  iunmbl2  18746  ioombl1  18751  uniioombllem6  18775  uniioombl  18776  dyadmax  18785  dyadmbllem  18786  opnmbllem  18788  subopnmbl  18791  volivth  18794  vitalilem2  18796  ismbf3d  18841  mbfimaopn2  18844  mbfaddlem  18847  mbfinf  18852  i1fmullem  18881  mbfi1fseqlem4  18905  mbfi1fseqlem6  18907  itg2const2  18928  itg2cnlem1  18948  itg2cn  18950  bddmulibl  19025  ellimc3  19061  limcflf  19063  dvlip  19172  dvlip2  19174  c1liplem1  19175  dvgt0lem1  19181  dvivthlem2  19188  dvne0  19190  lhop1lem  19192  lhop2  19194  lhop  19195  dvcnvre  19198  itgsubst  19228  mpfind  19260  mpfpf1  19266  pf1mpf  19267  tdeglem4  19278  mdegnn0cl  19289  ply1divex  19354  dvdsq1p  19378  ig1peu  19389  elply2  19410  plypf1  19426  plydivlem4  19508  plydivex  19509  elqaa  19534  aareccl  19538  aalioulem3  19546  aalioulem5  19548  aaliou  19550  ulmshftlem  19600  ulmcau  19604  ulmss  19606  ulmbdd  19607  ulmcn  19608  ulmdvlem3  19611  iblulm  19615  radcnvlem1  19621  radcnvlt1  19626  abelthlem5  19643  abelthlem8  19647  eflogeq  19787  efopn  19837  angpieqvd  19872  cxpeq  19965  dcubic  19974  xrlimcnp  20095  cxploglim  20104  amgm  20117  ftalem2  20143  ftalem7  20148  fta  20149  isppw2  20185  dchrptlem1  20335  dchrptlem2  20336  dchrptlem3  20337  dchrpt  20338  dchrsum2  20339  sumdchr2  20341  lgsne0  20404  lgsqr  20417  lgsdchrval  20418  lgsdchr  20419  lgsquadlem1  20425  2sqlem11  20446  dchrisumlem3  20472  dchrisum  20473  dchrvmasumif  20484  dchrisum0flb  20491  dchrisum0fno1  20492  rpvmasum2  20493  dchrisum0re  20494  dchrisum0lem3  20500  dchrisum0  20501  dchrmusum  20505  dchrvmasum  20506  chpdifbnd  20536  pntrlog2bnd  20565  pntibndlem3  20573  pntibnd  20574  pntlemi  20585  pntlem3  20590  pntleml  20592  ostth3  20619  ostth  20620  isgrp2d  20732  ghgrplem1  20863  nmobndi  21183  blocnilem  21212  ubthlem1  21279  ubthlem3  21281  htthlem  21327  shsel3  21724  omlsii  21812  spansncol  21977  pjspansn  21986  nmopun  22424  nmcexi  22436  riesz1  22475  elpjrn  22600  cvcon3  22694  chcv1  22765  atcvatlem  22795  chirredi  22804  erdszelem8  22900  erdszelem11  22903  erdsze2lem2  22906  cnpcon  22932  pconcon  22933  conpcon  22937  pconpi1  22939  sconpi1  22941  cnllyscon  22947  cvmsss2  22976  cvmcov2  22977  cvmfolem  22981  cvmliftmolem2  22984  cvmliftlem15  23000  cvmlift2lem1  23004  cvmlift2lem10  23014  cvmliftpht  23020  cvmlift3lem2  23022  cvmlift3lem4  23024  cvmlift3lem5  23025  eupai  23054  sinccvg  23177  dvdspw  23273  br8  23283  br6  23284  br4  23285  trpredtr  23401  frrlem5e  23457  axfelem20  23533  brcgr  23702  brbtwn2  23707  axbtwnid  23741  axcontlem2  23767  axcontlem7  23772  cgrtriv  23799  btwntriv2  23809  btwncomim  23810  btwnswapid  23814  btwnintr  23816  btwnexch3  23817  btwnouttr2  23819  ifscgr  23841  cgrxfr  23852  btwnxfr  23853  btwnconn3  23900  segcon2  23902  brsegle  23905  brsegle2  23906  seglecgr12im  23907  broutsideof3  23923  linethru  23950  elhf2  23979  iscnp4  24729  exopcopn  24738  flfnei2  24743  islimrs3  24747  altretop  24766  vtarsuelt  25061  abhp  25339  opnregcld  25414  cldregopn  25415  locfincmp  25470  comppfsc  25473  neibastop1  25474  neibastop2lem  25475  filbcmb  25598  sdclem1  25619  fdc  25621  fdc1  25622  incsequz  25624  caushft  25643  istotbnd3  25661  sstotbnd2  25664  sstotbnd  25665  sstotbnd3  25666  isbndx  25672  isbnd3  25674  ssbnd  25678  totbndbnd  25679  equivbnd  25680  prdsbnd2  25685  cntotbnd  25686  heibor1lem  25699  heibor1  25700  heiborlem9  25709  heibor  25711  bfplem2  25713  divrngidl  25819  prnc  25858  prtlem10  25899  elrfi  25935  isnacs3  25951  eldiophb  26002  diophrw  26004  eldioph2b  26008  diophin  26018  eldiophss  26020  diophrex  26021  rexrabdioph  26041  eldioph4b  26060  diophren  26062  rencldnfilem  26069  irrapxlem4  26076  irrapxlem6  26078  pellex  26086  pell1234qrdich  26112  pellfundex  26137  pellfund14b  26150  jm2.26a  26259  jm2.27  26267  fnwe2lem2  26314  lsmfgcl  26338  kercvrlsm  26347  lmhmfgima  26348  lmhmfgsplit  26350  lindfrn  26457  islinds4  26471  lpirlnr  26487  hbtlem2  26494  hbtlem4  26496  hbtlem5  26498  hbtlem6  26499  hbt  26500  mpaaeu  26521  rngunsnply  26544  psgnunilem3  26585  psgnghm  26603  lshpdisj  27866  cvrcon3b  28156  atnle  28196  hlhgt2  28267  hl0lt1N  28268  hl2at  28283  cvrexchlem  28297  cvratlem  28299  lvolnlelpln  28463  2lplnj  28498  ispsubcl2N  28825  lautcvr  28970  dva1dim  29863  dib1dim  30044  dib1dim2  30047  diclspsn  30073  dih1dimatlem  30208  dihlatat  30216  dihatexv  30217  dihatexv2  30218  dihjat2  30310  lcfrlem9  30429  lcfrlem16  30437  mapdrvallem2  30524  mapd1o  30527
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator