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

Theorem rexlimdva 2640
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 2639 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 2517
This theorem is referenced by:  rexlimdvaa  2641  rexlimivv  2645  rexlimdvv  2646  ralxfrd  4506  foco2  5600  elunirnALT  5699  f1elima  5707  grprinvlem  5978  grpridd  5980  tfrlem9a  6356  seqomlem2  6417  oawordexr  6508  odi  6531  oelimcl  6552  nnawordex  6589  nnaordex  6590  oaabs  6596  oaabs2  6597  omabs  6599  ectocld  6680  onfin  7005  dif1enOLD  7044  dif1en  7045  isfinite2  7069  isfiniteg  7071  fofinf1o  7091  fiin  7129  elfiun  7137  suplub2  7166  supisoex  7176  ordtypelem9  7195  ordtypelem10  7196  wemaplem3  7217  brwdom2  7241  brwdom3  7250  cantnflt  7327  oemapvali  7340  cantnflem4  7348  r1pwss  7410  rankr1ai  7424  infxpenc2lem1  7600  fseqenlem2  7606  fodomfi2  7641  infpwfien  7643  dfac12r  7726  ackbij1  7818  cff1  7838  fin23lem26  7905  fin23lem21  7919  isf32lem2  7934  fin1a2lem11  7990  fin1a2lem13  7992  ficard  8141  pwcfsdom  8159  fpwwe2  8219  pwfseqlem3  8236  gchina  8275  r1wunlim  8313  wunex2  8314  eltsk2g  8327  tskr1om2  8344  inttsk  8350  rankcf  8353  inatsk  8354  tskuni  8359  nqereu  8507  ltexnq  8553  1idpr  8607  suplem1pr  8630  supsrlem  8687  axpre-sup  8745  1re  8791  addcan  8950  addcan2  8951  negeu  8996  mulcand  9355  supmul1  9673  supmul  9676  suprzcl  10044  zsupss  10260  suprzcl2  10261  uzwo3  10264  qmulz  10272  qbtwnre  10478  xralrple  10484  ioo0  10633  ico0  10654  ioc0  10655  icc0  10656  fsequb  10989  expmulnbnd  11185  hashdom  11313  shftlem  11514  rexanuz  11780  rexuzre  11787  rexico  11788  caubnd  11793  limsupval2  11905  limsupgre  11906  limsupbnd1  11907  limsupbnd2  11908  rlim2lt  11922  rlim3  11923  lo1bdd2  11949  lo1bddrp  11950  o1lo1  11962  rlimclim1  11970  climuni  11977  climshftlem  11999  o1co  12011  rlimcn1  12013  climcn1  12016  o1rlimmul  12043  lo1le  12076  rlimno1  12078  isercoll  12092  caurcvg2  12101  serf0  12104  summolem2  12140  zsum  12142  fsumcvg3  12153  fsum2dlem  12184  fsumiun  12230  geomulcvg  12280  mertenslem2  12289  rpnnen2  12452  dvds1lem  12488  odd2np1lem  12534  odd2np1  12535  oexpneg  12538  bitsfi  12576  dvdssqim  12680  prmind2  12717  coprmdvds2  12730  isprm5  12739  rpexp  12747  pythagtriplem1  12817  iserodd  12836  pc2dvds  12879  pcprmpw2  12882  prmpwdvds  12899  pockthg  12901  prmreclem5  12915  1arith  12922  4sqlem11  12950  vdwapun  12969  vdwlem2  12977  vdwlem6  12981  vdwlem8  12983  vdwlem10  12985  vdwnnlem1  12990  vdwnnlem3  12992  0ram  13015  ramub1lem2  13022  ramcl  13024  firest  13285  imasvscafn  13387  ffthiso  13751  drsdirfi  14020  imasmnd2  14357  grprcan  14463  imasgrp2  14558  issubg4  14586  gaorber  14710  orbsta  14715  odmulg  14817  odbezout  14819  gexdvdsi  14842  sylow1lem3  14859  sylow1  14862  odcau  14863  pgpfi  14864  sylow2alem1  14876  slwhash  14883  sylow3lem2  14887  sylow3lem6  14891  lsmelvalm  14910  pj1id  14956  efgsfo  14996  efgredlemc  15002  efgrelexlemb  15007  efgredeu  15009  cyggeninv  15118  cygabl  15125  cygctb  15126  lt6abl  15129  ghmcyg  15130  cyggexb  15133  dprdssv  15199  dmdprdsplitlem  15220  dprddisj2  15222  dpjidcl  15241  ablfacrplem  15248  pgpfac1lem2  15258  pgpfac1lem4  15261  pgpfac1lem5  15262  pgpfaclem2  15265  pgpfaclem3  15266  ablfac2  15272  imasrng  15350  dvdsrcl2  15380  dvdsrmul1  15383  unitgrp  15397  irredrmul  15437  lss1d  15668  lssats2  15705  lspsn  15707  lmhmima  15752  lspsneleq  15816  lspsolv  15844  lpiss  15950  dvdsrz  16388  zlpirlem1  16389  znunit  16465  znrrg  16467  cygznlem3  16471  frgpcyg  16475  tgcl  16655  clsval2  16735  neiint  16789  neindisj  16802  innei  16810  restbas  16837  restcld  16851  restcldr  16853  restopnb  16854  ordtrest2lem  16881  pnfnei  16898  mnfnei  16899  cnpco  16944  cnprest  16965  lmss  16974  lmcls  16978  lmcnp  16980  pnrmopn  17019  haust1  17028  isnrm3  17035  isreg2  17053  ordthauslem  17059  cmpcovf  17066  cncmp  17067  cmpsub  17075  tgcmp  17076  hauscmplem  17081  t1conperf  17110  1stcfb  17119  1stcrest  17127  2ndcrest  17128  2ndcdisj  17130  2ndcomap  17132  dis2ndc  17134  1stccnp  17136  restnlly  17156  islly2  17158  nllyrest  17160  llyidm  17162  nllyidm  17163  hausllycmp  17168  cldllycmp  17169  lly1stc  17170  llycmpkgen2  17193  1stckgenlem  17196  ptbasfi  17224  txcnpi  17250  ptcnp  17264  pthaus  17280  txtube  17282  txcmplem1  17283  txcmplem2  17284  txlm  17290  xkohaus  17295  xkococnlem  17301  xkococn  17302  basqtop  17350  tgqtop  17351  kqfvima  17369  regr1lem  17378  kqreglem1  17380  kqreglem2  17381  kqnrmlem1  17382  kqnrmlem2  17383  reghmph  17432  nrmhmph  17433  qtophmeo  17456  fbssfi  17480  trfbas2  17486  isfild  17501  fgcl  17521  fgabs  17522  neifil  17523  filuni  17528  trfil2  17530  trfg  17534  isufil2  17551  ssufl  17561  ufileu  17562  uffix  17564  rnelfm  17596  fmfnfmlem2  17598  fmfnfmlem4  17600  fmfnfm  17601  fmufil  17602  fmco  17604  ufldom  17605  fclsopn  17657  fclsfnflim  17670  uffclsflim  17674  ufilcmp  17675  cnpfcfi  17683  cnpfcf  17684  alexsublem  17686  alexsubALT  17693  ptcmplem3  17696  ptcmplem4  17697  cldsubg  17741  ghmcnp  17745  divstgpopn  17750  tsmsgsum  17769  tsmsres  17774  tsmsxplem1  17783  tsmsxp  17785  imasdsf1olem  17885  blss  17920  blssex  17921  mopni3  17988  blcld  17999  met1stc  18015  met2ndci  18016  metrest  18018  prdsxmslem2  18023  metcnp3  18034  metcnpi3  18040  qdensere  18227  reperflem  18271  icccmplem1  18275  icccmplem3  18277  opnreen  18284  xrge0tsms  18287  metdseq0  18306  mulc1cncf  18357  cncfco  18359  cnheibor  18401  cnllycmp  18402  bndth  18404  lebnumlem1  18407  lebnumlem3  18409  lebnum  18410  xlebnum  18411  lebnumii  18412  pi1blem  18485  nmoleub2lem3  18544  nmhmcn  18549  cfil3i  18643  iscfil3  18647  cfilfcls  18648  cmetcaulem  18662  iscmet3lem2  18666  cfilres  18670  lmle  18675  cmetss  18688  relcmpcmet  18690  bcthlem4  18697  bcthlem5  18698  pjthlem2  18750  ivthlem2  18760  ivthlem3  18761  ivthicc  18766  cniccbdd  18769  ovolunlem1  18804  ovoliunlem2  18810  ovolshftlem2  18817  ovolscalem2  18821  ovolicc2lem4  18827  ovolicc2lem5  18828  ovolicc2  18829  nulmbl2  18842  iundisj  18853  volsup  18861  iunmbl2  18862  ioombl1  18867  uniioombllem6  18891  uniioombl  18892  dyadmax  18901  dyadmbllem  18902  opnmbllem  18904  subopnmbl  18907  volivth  18910  vitalilem2  18912  ismbf3d  18957  mbfimaopn2  18960  mbfaddlem  18963  mbfinf  18968  i1fmullem  18997  mbfi1fseqlem4  19021  mbfi1fseqlem6  19023  itg2const2  19044  itg2cnlem1  19064  itg2cn  19066  bddmulibl  19141  ellimc3  19177  limcflf  19179  dvlip  19288  dvlip2  19290  c1liplem1  19291  dvgt0lem1  19297  dvivthlem2  19304  dvne0  19306  lhop1lem  19308  lhop2  19310  lhop  19311  dvcnvre  19314  itgsubst  19344  mpfind  19376  mpfpf1  19382  pf1mpf  19383  tdeglem4  19394  mdegnn0cl  19405  ply1divex  19470  dvdsq1p  19494  ig1peu  19505  elply2  19526  plypf1  19542  plydivlem4  19624  plydivex  19625  elqaa  19650  aareccl  19654  aalioulem3  19662  aalioulem5  19664  aaliou  19666  ulmshftlem  19716  ulmcau  19720  ulmss  19722  ulmbdd  19723  ulmcn  19724  ulmdvlem3  19727  iblulm  19731  radcnvlem1  19737  radcnvlt1  19742  abelthlem5  19759  abelthlem8  19763  eflogeq  19903  efopn  19953  cxpeq  20045  angpieqvd  20076  dcubic  20090  xrlimcnp  20211  cxploglim  20220  amgm  20233  ftalem2  20259  ftalem7  20264  fta  20265  isppw2  20301  dchrptlem1  20451  dchrptlem2  20452  dchrptlem3  20453  dchrpt  20454  dchrsum2  20455  sumdchr2  20457  lgsne0  20520  lgsqr  20533  lgsdchrval  20534  lgsdchr  20535  lgsquadlem1  20541  2sqlem11  20562  dchrisumlem3  20588  dchrisum  20589  dchrvmasumif  20600  dchrisum0flb  20607  dchrisum0fno1  20608  rpvmasum2  20609  dchrisum0re  20610  dchrisum0lem3  20616  dchrisum0  20617  dchrmusum  20621  dchrvmasum  20622  chpdifbnd  20652  pntrlog2bnd  20681  pntibndlem3  20689  pntibnd  20690  pntlemi  20701  pntlem3  20706  pntleml  20708  ostth3  20735  ostth  20736  isgrp2d  20848  ghgrplem1  20979  nmobndi  21299  blocnilem  21328  ubthlem1  21395  ubthlem3  21397  htthlem  21443  shsel3  21840  omlsii  21928  spansncol  22093  pjspansn  22102  nmopun  22540  nmcexi  22552  riesz1  22591  elpjrn  22716  cvcon3  22810  chcv1  22881  atcvatlem  22911  chirredi  22920  erdszelem8  23087  erdszelem11  23090  erdsze2lem2  23093  cnpcon  23119  pconcon  23120  conpcon  23124  pconpi1  23126  sconpi1  23128  cnllyscon  23134  cvmsss2  23163  cvmcov2  23164  cvmfolem  23168  cvmliftmolem2  23171  cvmliftlem15  23187  cvmlift2lem1  23191  cvmlift2lem10  23201  cvmliftpht  23207  cvmlift3lem2  23209  cvmlift3lem4  23211  cvmlift3lem5  23212  eupai  23241  sinccvg  23364  dvdspw  23460  br8  23470  br6  23471  br4  23472  trpredtr  23588  frrlem5e  23644  axfelem20  23720  brcgr  23889  brbtwn2  23894  axbtwnid  23928  axcontlem2  23954  axcontlem7  23959  cgrtriv  23986  btwntriv2  23996  btwncomim  23997  btwnswapid  24001  btwnintr  24003  btwnexch3  24004  btwnouttr2  24006  ifscgr  24028  cgrxfr  24039  btwnxfr  24040  btwnconn3  24087  segcon2  24089  brsegle  24092  brsegle2  24093  seglecgr12im  24094  broutsideof3  24110  linethru  24137  elhf2  24166  iscnp4  24916  exopcopn  24925  flfnei2  24930  islimrs3  24934  altretop  24953  vtarsuelt  25248  abhp  25526  opnregcld  25601  cldregopn  25602  locfincmp  25657  comppfsc  25660  neibastop1  25661  neibastop2lem  25662  filbcmb  25785  sdclem1  25806  fdc  25808  fdc1  25809  incsequz  25811  caushft  25830  istotbnd3  25848  sstotbnd2  25851  sstotbnd  25852  sstotbnd3  25853  isbndx  25859  isbnd3  25861  ssbnd  25865  totbndbnd  25866  equivbnd  25867  prdsbnd2  25872  cntotbnd  25873  heibor1lem  25886  heibor1  25887  heiborlem9  25896  heibor  25898  bfplem2  25900  divrngidl  26006  prnc  26045  prtlem10  26086  elrfi  26122  isnacs3  26138  eldiophb  26189  diophrw  26191  eldioph2b  26195  diophin  26205  eldiophss  26207  diophrex  26208  rexrabdioph  26228  eldioph4b  26247  diophren  26249  rencldnfilem  26256  irrapxlem4  26263  irrapxlem6  26265  pellex  26273  pell1234qrdich  26299  pellfundex  26324  pellfund14b  26337  jm2.26a  26446  jm2.27  26454  fnwe2lem2  26501  lsmfgcl  26525  kercvrlsm  26534  lmhmfgima  26535  lmhmfgsplit  26537  lindfrn  26644  islinds4  26658  lpirlnr  26674  hbtlem2  26681  hbtlem4  26683  hbtlem5  26685  hbtlem6  26686  hbt  26687  mpaaeu  26708  rngunsnply  26731  psgnunilem3  26772  psgnghm  26790  lshpdisj  28328  cvrcon3b  28618  atnle  28658  hlhgt2  28729  hl0lt1N  28730  hl2at  28745  cvrexchlem  28759  cvratlem  28761  lvolnlelpln  28925  2lplnj  28960  ispsubcl2N  29287  lautcvr  29432  dva1dim  30325  dib1dim  30506  dib1dim2  30509  diclspsn  30535  dih1dimatlem  30670  dihlatat  30678  dihatexv  30679  dihatexv2  30680  dihjat2  30772  lcfrlem9  30891  lcfrlem16  30899  mapdrvallem2  30986  mapd1o  30989
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 2521  df-rex 2522
  Copyright terms: Public domain W3C validator