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

Theorem rexlimdva 2667
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 423 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2666 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rexlimdvaa  2668  rexlimivv  2672  rexlimdvv  2673  ralxfrd  4548  foco2  5680  elunirnALT  5779  f1elima  5787  grprinvlem  6058  grpridd  6060  tfrlem9a  6402  seqomlem2  6463  oawordexr  6554  odi  6577  oelimcl  6598  nnawordex  6635  nnaordex  6636  oaabs  6642  oaabs2  6643  omabs  6645  ectocld  6726  onfin  7051  dif1enOLD  7090  dif1en  7091  isfinite2  7115  isfiniteg  7117  fofinf1o  7137  fiin  7175  elfiun  7183  suplub2  7212  supisoex  7222  ordtypelem9  7241  ordtypelem10  7242  wemaplem3  7263  brwdom2  7287  brwdom3  7296  cantnflt  7373  oemapvali  7386  cantnflem4  7394  r1pwss  7456  rankr1ai  7470  infxpenc2lem1  7646  fseqenlem2  7652  fodomfi2  7687  infpwfien  7689  dfac12r  7772  ackbij1  7864  cff1  7884  fin23lem26  7951  fin23lem21  7965  isf32lem2  7980  fin1a2lem11  8036  fin1a2lem13  8038  ficard  8187  pwcfsdom  8205  fpwwe2  8265  pwfseqlem3  8282  gchina  8321  r1wunlim  8359  wunex2  8360  eltsk2g  8373  tskr1om2  8390  inttsk  8396  rankcf  8399  inatsk  8400  tskuni  8405  nqereu  8553  ltexnq  8599  1idpr  8653  suplem1pr  8676  supsrlem  8733  axpre-sup  8791  1re  8837  addcan  8996  addcan2  8997  negeu  9042  mulcand  9401  supmul1  9719  supmul  9722  suprzcl  10091  zsupss  10307  suprzcl2  10308  uzwo3  10311  qmulz  10319  qbtwnre  10526  xralrple  10532  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  fsequb  11037  expmulnbnd  11233  hashdom  11361  shftlem  11563  rexanuz  11829  rexuzre  11836  rexico  11837  caubnd  11842  limsupval2  11954  limsupgre  11955  limsupbnd1  11956  limsupbnd2  11957  rlim2lt  11971  rlim3  11972  lo1bdd2  11998  lo1bddrp  11999  o1lo1  12011  rlimclim1  12019  climuni  12026  climshftlem  12048  o1co  12060  rlimcn1  12062  climcn1  12065  o1rlimmul  12092  lo1le  12125  rlimno1  12127  isercoll  12141  caurcvg2  12150  serf0  12153  summolem2  12189  zsum  12191  fsumcvg3  12202  fsum2dlem  12233  fsumiun  12279  geomulcvg  12332  mertenslem2  12341  rpnnen2  12504  dvds1lem  12540  odd2np1lem  12586  odd2np1  12587  oexpneg  12590  bitsfi  12628  dvdssqim  12732  prmind2  12769  coprmdvds2  12782  isprm5  12791  rpexp  12799  pythagtriplem1  12869  iserodd  12888  pc2dvds  12931  pcprmpw2  12934  prmpwdvds  12951  pockthg  12953  prmreclem5  12967  1arith  12974  4sqlem11  13002  vdwapun  13021  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  vdwlem10  13037  vdwnnlem1  13042  vdwnnlem3  13044  0ram  13067  ramub1lem2  13074  ramcl  13076  firest  13337  imasvscafn  13439  ffthiso  13803  drsdirfi  14072  imasmnd2  14409  grprcan  14515  imasgrp2  14610  issubg4  14638  gaorber  14762  orbsta  14767  odmulg  14869  odbezout  14871  gexdvdsi  14894  sylow1lem3  14911  sylow1  14914  odcau  14915  pgpfi  14916  sylow2alem1  14928  slwhash  14935  sylow3lem2  14939  sylow3lem6  14943  lsmelvalm  14962  pj1id  15008  efgsfo  15048  efgredlemc  15054  efgrelexlemb  15059  efgredeu  15061  cyggeninv  15170  cygabl  15177  cygctb  15178  lt6abl  15181  ghmcyg  15182  cyggexb  15185  dprdssv  15251  dmdprdsplitlem  15272  dprddisj2  15274  dpjidcl  15293  ablfacrplem  15300  pgpfac1lem2  15310  pgpfac1lem4  15313  pgpfac1lem5  15314  pgpfaclem2  15317  pgpfaclem3  15318  ablfac2  15324  imasrng  15402  dvdsrcl2  15432  dvdsrmul1  15435  unitgrp  15449  irredrmul  15489  lss1d  15720  lssats2  15757  lspsn  15759  lmhmima  15804  lspsneleq  15868  lspsolv  15896  lpiss  16002  dvdsrz  16440  zlpirlem1  16441  znunit  16517  znrrg  16519  cygznlem3  16523  frgpcyg  16527  tgcl  16707  clsval2  16787  neiint  16841  neindisj  16854  innei  16862  restbas  16889  restcld  16903  restcldr  16905  restopnb  16906  ordtrest2lem  16933  pnfnei  16950  mnfnei  16951  cnpco  16996  cnprest  17017  lmss  17026  lmcls  17030  lmcnp  17032  pnrmopn  17071  haust1  17080  isnrm3  17087  isreg2  17105  ordthauslem  17111  cmpcovf  17118  cncmp  17119  cmpsub  17127  tgcmp  17128  hauscmplem  17133  t1conperf  17162  1stcfb  17171  1stcrest  17179  2ndcrest  17180  2ndcdisj  17182  2ndcomap  17184  dis2ndc  17186  1stccnp  17188  restnlly  17208  islly2  17210  nllyrest  17212  llyidm  17214  nllyidm  17215  hausllycmp  17220  cldllycmp  17221  lly1stc  17222  llycmpkgen2  17245  1stckgenlem  17248  ptbasfi  17276  txcnpi  17302  ptcnp  17316  pthaus  17332  txtube  17334  txcmplem1  17335  txcmplem2  17336  txlm  17342  xkohaus  17347  xkococnlem  17353  xkococn  17354  basqtop  17402  tgqtop  17403  kqfvima  17421  regr1lem  17430  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  reghmph  17484  nrmhmph  17485  qtophmeo  17508  fbssfi  17532  trfbas2  17538  isfild  17553  fgcl  17573  fgabs  17574  neifil  17575  filuni  17580  trfil2  17582  trfg  17586  isufil2  17603  ssufl  17613  ufileu  17614  uffix  17616  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  fmufil  17654  fmco  17656  ufldom  17657  fclsopn  17709  fclsfnflim  17722  uffclsflim  17726  ufilcmp  17727  cnpfcfi  17735  cnpfcf  17736  alexsublem  17738  alexsubALT  17745  ptcmplem3  17748  ptcmplem4  17749  cldsubg  17793  ghmcnp  17797  divstgpopn  17802  tsmsgsum  17821  tsmsres  17826  tsmsxplem1  17835  tsmsxp  17837  imasdsf1olem  17937  blss  17972  blssex  17973  mopni3  18040  blcld  18051  met1stc  18067  met2ndci  18068  metrest  18070  prdsxmslem2  18075  metcnp3  18086  metcnpi3  18092  qdensere  18279  reperflem  18323  icccmplem1  18327  icccmplem3  18329  opnreen  18336  xrge0tsms  18339  metdseq0  18358  mulc1cncf  18409  cncfco  18411  cnheibor  18453  cnllycmp  18454  bndth  18456  lebnumlem1  18459  lebnumlem3  18461  lebnum  18462  xlebnum  18463  lebnumii  18464  pi1blem  18537  nmoleub2lem3  18596  nmhmcn  18601  cfil3i  18695  iscfil3  18699  cfilfcls  18700  cmetcaulem  18714  iscmet3lem2  18718  cfilres  18722  lmle  18727  cmetss  18740  relcmpcmet  18742  bcthlem4  18749  bcthlem5  18750  pjthlem2  18802  ivthlem2  18812  ivthlem3  18813  ivthicc  18818  cniccbdd  18821  ovolunlem1  18856  ovoliunlem2  18862  ovolshftlem2  18869  ovolscalem2  18873  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  nulmbl2  18894  iundisj  18905  volsup  18913  iunmbl2  18914  ioombl1  18919  uniioombllem6  18943  uniioombl  18944  dyadmax  18953  dyadmbllem  18954  opnmbllem  18956  subopnmbl  18959  volivth  18962  vitalilem2  18964  ismbf3d  19009  mbfimaopn2  19012  mbfaddlem  19015  mbfinf  19020  i1fmullem  19049  mbfi1fseqlem4  19073  mbfi1fseqlem6  19075  itg2const2  19096  itg2cnlem1  19116  itg2cn  19118  bddmulibl  19193  ellimc3  19229  limcflf  19231  dvlip  19340  dvlip2  19342  c1liplem1  19343  dvgt0lem1  19349  dvivthlem2  19356  dvne0  19358  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvre  19366  itgsubst  19396  mpfind  19428  mpfpf1  19434  pf1mpf  19435  tdeglem4  19446  mdegnn0cl  19457  ply1divex  19522  dvdsq1p  19546  ig1peu  19557  elply2  19578  plypf1  19594  plydivlem4  19676  plydivex  19677  elqaa  19702  aareccl  19706  aalioulem3  19714  aalioulem5  19716  aaliou  19718  ulmshftlem  19768  ulmcau  19772  ulmss  19774  ulmbdd  19775  ulmcn  19776  ulmdvlem3  19779  iblulm  19783  radcnvlem1  19789  radcnvlt1  19794  abelthlem5  19811  abelthlem8  19815  eflogeq  19955  efopn  20005  cxpeq  20097  angpieqvd  20128  dcubic  20142  xrlimcnp  20263  cxploglim  20272  amgm  20285  ftalem2  20311  ftalem7  20316  fta  20317  isppw2  20353  dchrptlem1  20503  dchrptlem2  20504  dchrptlem3  20505  dchrpt  20506  dchrsum2  20507  sumdchr2  20509  lgsne0  20572  lgsqr  20585  lgsdchrval  20586  lgsdchr  20587  lgsquadlem1  20593  2sqlem11  20614  dchrisumlem3  20640  dchrisum  20641  dchrvmasumif  20652  dchrisum0flb  20659  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem3  20668  dchrisum0  20669  dchrmusum  20673  dchrvmasum  20674  chpdifbnd  20704  pntrlog2bnd  20733  pntibndlem3  20741  pntibnd  20742  pntlemi  20753  pntlem3  20758  pntleml  20760  ostth3  20787  ostth  20788  isgrp2d  20902  ghgrplem1  21033  nmobndi  21353  blocnilem  21382  ubthlem1  21449  ubthlem3  21451  htthlem  21497  shsel3  21894  omlsii  21982  spansncol  22147  pjspansn  22156  nmopun  22594  nmcexi  22606  riesz1  22645  elpjrn  22770  cvcon3  22864  chcv1  22935  atcvatlem  22965  chirredi  22974  xmulcand  23104  iundisjfi  23363  pnfneige0  23374  lmxrge0  23375  xrge0tsmsd  23382  esumpcvgval  23446  measdivcstOLD  23551  measdivcst  23552  erdszelem8  23729  erdszelem11  23732  erdsze2lem2  23735  cnpcon  23761  pconcon  23762  conpcon  23766  pconpi1  23768  sconpi1  23770  cnllyscon  23776  cvmsss2  23805  cvmcov2  23806  cvmfolem  23810  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift2lem1  23833  cvmlift2lem10  23843  cvmliftpht  23849  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3lem5  23854  eupai  23883  sinccvg  24006  dvdspw  24103  br8  24113  br6  24114  br4  24115  trpredtr  24233  frrlem5e  24289  brcgr  24528  brbtwn2  24533  axbtwnid  24567  axcontlem2  24593  axcontlem7  24598  cgrtriv  24625  btwntriv2  24635  btwncomim  24636  btwnswapid  24640  btwnintr  24642  btwnexch3  24643  btwnouttr2  24645  ifscgr  24667  cgrxfr  24678  btwnxfr  24679  btwnconn3  24726  segcon2  24728  brsegle  24731  brsegle2  24732  seglecgr12im  24733  broutsideof3  24749  linethru  24776  elhf2  24805  iscnp4  25563  exopcopn  25572  flfnei2  25577  islimrs3  25581  altretop  25600  vtarsuelt  25895  abhp  26173  opnregcld  26248  cldregopn  26249  locfincmp  26304  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  filbcmb  26432  sdclem1  26453  fdc  26455  fdc1  26456  incsequz  26458  caushft  26477  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  sstotbnd3  26500  isbndx  26506  isbnd3  26508  ssbnd  26512  totbndbnd  26513  equivbnd  26514  prdsbnd2  26519  cntotbnd  26520  heibor1lem  26533  heibor1  26534  heiborlem9  26543  heibor  26545  bfplem2  26547  divrngidl  26653  prnc  26692  prtlem10  26733  elrfi  26769  isnacs3  26785  eldiophb  26836  diophrw  26838  eldioph2b  26842  diophin  26852  eldiophss  26854  diophrex  26855  rexrabdioph  26875  eldioph4b  26894  diophren  26896  rencldnfilem  26903  irrapxlem4  26910  irrapxlem6  26912  pellex  26920  pell1234qrdich  26946  pellfundex  26971  pellfund14b  26984  jm2.26a  27093  jm2.27  27101  fnwe2lem2  27148  lsmfgcl  27172  kercvrlsm  27181  lmhmfgima  27182  lmhmfgsplit  27184  lindfrn  27291  islinds4  27305  lpirlnr  27321  hbtlem2  27328  hbtlem4  27330  hbtlem5  27332  hbtlem6  27333  hbt  27334  mpaaeu  27355  rngunsnply  27378  psgnunilem3  27419  psgnghm  27437  lshpdisj  29177  cvrcon3b  29467  atnle  29507  hlhgt2  29578  hl0lt1N  29579  hl2at  29594  cvrexchlem  29608  cvratlem  29610  lvolnlelpln  29774  2lplnj  29809  ispsubcl2N  30136  lautcvr  30281  dva1dim  31174  dib1dim  31355  dib1dim2  31358  diclspsn  31384  dih1dimatlem  31519  dihlatat  31527  dihatexv  31528  dihatexv2  31529  dihjat2  31621  lcfrlem9  31740  lcfrlem16  31748  mapdrvallem2  31835  mapd1o  31838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator