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

Theorem rexlimdva 2680
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 2679 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  rexlimdvaa  2681  rexlimivv  2685  rexlimdvv  2686  ralxfrd  4564  foco2  5696  elunirnALT  5795  f1elima  5803  grprinvlem  6074  grpridd  6076  tfrlem9a  6418  seqomlem2  6479  oawordexr  6570  odi  6593  oelimcl  6614  nnawordex  6651  nnaordex  6652  oaabs  6658  oaabs2  6659  omabs  6661  ectocld  6742  onfin  7067  dif1enOLD  7106  dif1en  7107  isfinite2  7131  isfiniteg  7133  fofinf1o  7153  fiin  7191  elfiun  7199  suplub2  7228  supisoex  7238  ordtypelem9  7257  ordtypelem10  7258  wemaplem3  7279  brwdom2  7303  brwdom3  7312  cantnflt  7389  oemapvali  7402  cantnflem4  7410  r1pwss  7472  rankr1ai  7486  infxpenc2lem1  7662  fseqenlem2  7668  fodomfi2  7703  infpwfien  7705  dfac12r  7788  ackbij1  7880  cff1  7900  fin23lem26  7967  fin23lem21  7981  isf32lem2  7996  fin1a2lem11  8052  fin1a2lem13  8054  ficard  8203  pwcfsdom  8221  fpwwe2  8281  pwfseqlem3  8298  gchina  8337  r1wunlim  8375  wunex2  8376  eltsk2g  8389  tskr1om2  8406  inttsk  8412  rankcf  8415  inatsk  8416  tskuni  8421  nqereu  8569  ltexnq  8615  1idpr  8669  suplem1pr  8692  supsrlem  8749  axpre-sup  8807  1re  8853  addcan  9012  addcan2  9013  negeu  9058  mulcand  9417  supmul1  9735  supmul  9738  suprzcl  10107  zsupss  10323  suprzcl2  10324  uzwo3  10327  qmulz  10335  qbtwnre  10542  xralrple  10548  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  fsequb  11053  expmulnbnd  11249  hashdom  11377  shftlem  11579  rexanuz  11845  rexuzre  11852  rexico  11853  caubnd  11858  limsupval2  11970  limsupgre  11971  limsupbnd1  11972  limsupbnd2  11973  rlim2lt  11987  rlim3  11988  lo1bdd2  12014  lo1bddrp  12015  o1lo1  12027  rlimclim1  12035  climuni  12042  climshftlem  12064  o1co  12076  rlimcn1  12078  climcn1  12081  o1rlimmul  12108  lo1le  12141  rlimno1  12143  isercoll  12157  caurcvg2  12166  serf0  12169  summolem2  12205  zsum  12207  fsumcvg3  12218  fsum2dlem  12249  fsumiun  12295  geomulcvg  12348  mertenslem2  12357  rpnnen2  12520  dvds1lem  12556  odd2np1lem  12602  odd2np1  12603  oexpneg  12606  bitsfi  12644  dvdssqim  12748  prmind2  12785  coprmdvds2  12798  isprm5  12807  rpexp  12815  pythagtriplem1  12885  iserodd  12904  pc2dvds  12947  pcprmpw2  12950  prmpwdvds  12967  pockthg  12969  prmreclem5  12983  1arith  12990  4sqlem11  13018  vdwapun  13037  vdwlem2  13045  vdwlem6  13049  vdwlem8  13051  vdwlem10  13053  vdwnnlem1  13058  vdwnnlem3  13060  0ram  13083  ramub1lem2  13090  ramcl  13092  firest  13353  imasvscafn  13455  ffthiso  13819  drsdirfi  14088  imasmnd2  14425  grprcan  14531  imasgrp2  14626  issubg4  14654  gaorber  14778  orbsta  14783  odmulg  14885  odbezout  14887  gexdvdsi  14910  sylow1lem3  14927  sylow1  14930  odcau  14931  pgpfi  14932  sylow2alem1  14944  slwhash  14951  sylow3lem2  14955  sylow3lem6  14959  lsmelvalm  14978  pj1id  15024  efgsfo  15064  efgredlemc  15070  efgrelexlemb  15075  efgredeu  15077  cyggeninv  15186  cygabl  15193  cygctb  15194  lt6abl  15197  ghmcyg  15198  cyggexb  15201  dprdssv  15267  dmdprdsplitlem  15288  dprddisj2  15290  dpjidcl  15309  ablfacrplem  15316  pgpfac1lem2  15326  pgpfac1lem4  15329  pgpfac1lem5  15330  pgpfaclem2  15333  pgpfaclem3  15334  ablfac2  15340  imasrng  15418  dvdsrcl2  15448  dvdsrmul1  15451  unitgrp  15465  irredrmul  15505  lss1d  15736  lssats2  15773  lspsn  15775  lmhmima  15820  lspsneleq  15884  lspsolv  15912  lpiss  16018  dvdsrz  16456  zlpirlem1  16457  znunit  16533  znrrg  16535  cygznlem3  16539  frgpcyg  16543  tgcl  16723  clsval2  16803  neiint  16857  neindisj  16870  innei  16878  restbas  16905  restcld  16919  restcldr  16921  restopnb  16922  ordtrest2lem  16949  pnfnei  16966  mnfnei  16967  cnpco  17012  cnprest  17033  lmss  17042  lmcls  17046  lmcnp  17048  pnrmopn  17087  haust1  17096  isnrm3  17103  isreg2  17121  ordthauslem  17127  cmpcovf  17134  cncmp  17135  cmpsub  17143  tgcmp  17144  hauscmplem  17149  t1conperf  17178  1stcfb  17187  1stcrest  17195  2ndcrest  17196  2ndcdisj  17198  2ndcomap  17200  dis2ndc  17202  1stccnp  17204  restnlly  17224  islly2  17226  nllyrest  17228  llyidm  17230  nllyidm  17231  hausllycmp  17236  cldllycmp  17237  lly1stc  17238  llycmpkgen2  17261  1stckgenlem  17264  ptbasfi  17292  txcnpi  17318  ptcnp  17332  pthaus  17348  txtube  17350  txcmplem1  17351  txcmplem2  17352  txlm  17358  xkohaus  17363  xkococnlem  17369  xkococn  17370  basqtop  17418  tgqtop  17419  kqfvima  17437  regr1lem  17446  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  reghmph  17500  nrmhmph  17501  qtophmeo  17524  fbssfi  17548  trfbas2  17554  isfild  17569  fgcl  17589  fgabs  17590  neifil  17591  filuni  17596  trfil2  17598  trfg  17602  isufil2  17619  ssufl  17629  ufileu  17630  uffix  17632  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  fmufil  17670  fmco  17672  ufldom  17673  fclsopn  17725  fclsfnflim  17738  uffclsflim  17742  ufilcmp  17743  cnpfcfi  17751  cnpfcf  17752  alexsublem  17754  alexsubALT  17761  ptcmplem3  17764  ptcmplem4  17765  cldsubg  17809  ghmcnp  17813  divstgpopn  17818  tsmsgsum  17837  tsmsres  17842  tsmsxplem1  17851  tsmsxp  17853  imasdsf1olem  17953  blss  17988  blssex  17989  mopni3  18056  blcld  18067  met1stc  18083  met2ndci  18084  metrest  18086  prdsxmslem2  18091  metcnp3  18102  metcnpi3  18108  qdensere  18295  reperflem  18339  icccmplem1  18343  icccmplem3  18345  opnreen  18352  xrge0tsms  18355  metdseq0  18374  mulc1cncf  18425  cncfco  18427  cnheibor  18469  cnllycmp  18470  bndth  18472  lebnumlem1  18475  lebnumlem3  18477  lebnum  18478  xlebnum  18479  lebnumii  18480  pi1blem  18553  nmoleub2lem3  18612  nmhmcn  18617  cfil3i  18711  iscfil3  18715  cfilfcls  18716  cmetcaulem  18730  iscmet3lem2  18734  cfilres  18738  lmle  18743  cmetss  18756  relcmpcmet  18758  bcthlem4  18765  bcthlem5  18766  pjthlem2  18818  ivthlem2  18828  ivthlem3  18829  ivthicc  18834  cniccbdd  18837  ovolunlem1  18872  ovoliunlem2  18878  ovolshftlem2  18885  ovolscalem2  18889  ovolicc2lem4  18895  ovolicc2lem5  18896  ovolicc2  18897  nulmbl2  18910  iundisj  18921  volsup  18929  iunmbl2  18930  ioombl1  18935  uniioombllem6  18959  uniioombl  18960  dyadmax  18969  dyadmbllem  18970  opnmbllem  18972  subopnmbl  18975  volivth  18978  vitalilem2  18980  ismbf3d  19025  mbfimaopn2  19028  mbfaddlem  19031  mbfinf  19036  i1fmullem  19065  mbfi1fseqlem4  19089  mbfi1fseqlem6  19091  itg2const2  19112  itg2cnlem1  19132  itg2cn  19134  bddmulibl  19209  ellimc3  19245  limcflf  19247  dvlip  19356  dvlip2  19358  c1liplem1  19359  dvgt0lem1  19365  dvivthlem2  19372  dvne0  19374  lhop1lem  19376  lhop2  19378  lhop  19379  dvcnvre  19382  itgsubst  19412  mpfind  19444  mpfpf1  19450  pf1mpf  19451  tdeglem4  19462  mdegnn0cl  19473  ply1divex  19538  dvdsq1p  19562  ig1peu  19573  elply2  19594  plypf1  19610  plydivlem4  19692  plydivex  19693  elqaa  19718  aareccl  19722  aalioulem3  19730  aalioulem5  19732  aaliou  19734  ulmshftlem  19784  ulmcau  19788  ulmss  19790  ulmbdd  19791  ulmcn  19792  ulmdvlem3  19795  iblulm  19799  radcnvlem1  19805  radcnvlt1  19810  abelthlem5  19827  abelthlem8  19831  eflogeq  19971  efopn  20021  cxpeq  20113  angpieqvd  20144  dcubic  20158  xrlimcnp  20279  cxploglim  20288  amgm  20301  ftalem2  20327  ftalem7  20332  fta  20333  isppw2  20369  dchrptlem1  20519  dchrptlem2  20520  dchrptlem3  20521  dchrpt  20522  dchrsum2  20523  sumdchr2  20525  lgsne0  20588  lgsqr  20601  lgsdchrval  20602  lgsdchr  20603  lgsquadlem1  20609  2sqlem11  20630  dchrisumlem3  20656  dchrisum  20657  dchrvmasumif  20668  dchrisum0flb  20675  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem3  20684  dchrisum0  20685  dchrmusum  20689  dchrvmasum  20690  chpdifbnd  20720  pntrlog2bnd  20749  pntibndlem3  20757  pntibnd  20758  pntlemi  20769  pntlem3  20774  pntleml  20776  ostth3  20803  ostth  20804  isgrp2d  20918  ghgrplem1  21049  nmobndi  21369  blocnilem  21398  ubthlem1  21465  ubthlem3  21467  htthlem  21513  shsel3  21910  omlsii  21998  spansncol  22163  pjspansn  22172  nmopun  22610  nmcexi  22622  riesz1  22661  elpjrn  22786  cvcon3  22880  chcv1  22951  atcvatlem  22981  chirredi  22990  xmulcand  23120  iundisjfi  23378  pnfneige0  23389  lmxrge0  23390  xrge0tsmsd  23397  esumpcvgval  23461  measdivcstOLD  23566  measdivcst  23567  erdszelem8  23744  erdszelem11  23747  erdsze2lem2  23750  cnpcon  23776  pconcon  23777  conpcon  23781  pconpi1  23783  sconpi1  23785  cnllyscon  23791  cvmsss2  23820  cvmcov2  23821  cvmfolem  23825  cvmliftmolem2  23828  cvmliftlem15  23844  cvmlift2lem1  23848  cvmlift2lem10  23858  cvmliftpht  23864  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3lem5  23869  eupai  23898  sinccvg  24021  zprod  24160  dvdspw  24174  br8  24184  br6  24185  br4  24186  trpredtr  24304  frrlem5e  24360  brcgr  24600  brbtwn2  24605  axbtwnid  24639  axcontlem2  24665  axcontlem7  24670  cgrtriv  24697  btwntriv2  24707  btwncomim  24708  btwnswapid  24712  btwnintr  24714  btwnexch3  24715  btwnouttr2  24717  ifscgr  24739  cgrxfr  24750  btwnxfr  24751  btwnconn3  24798  segcon2  24800  brsegle  24803  brsegle2  24804  seglecgr12im  24805  broutsideof3  24821  linethru  24848  elhf2  24877  supaddc  24995  supadd  24996  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  bddiblnc  25021  iscnp4  25666  exopcopn  25675  flfnei2  25680  islimrs3  25684  altretop  25703  vtarsuelt  25998  abhp  26276  opnregcld  26351  cldregopn  26352  locfincmp  26407  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  filbcmb  26535  sdclem1  26556  fdc  26558  fdc1  26559  incsequz  26561  caushft  26580  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  sstotbnd3  26603  isbndx  26609  isbnd3  26611  ssbnd  26615  totbndbnd  26616  equivbnd  26617  prdsbnd2  26622  cntotbnd  26623  heibor1lem  26636  heibor1  26637  heiborlem9  26646  heibor  26648  bfplem2  26650  divrngidl  26756  prnc  26795  prtlem10  26836  elrfi  26872  isnacs3  26888  eldiophb  26939  diophrw  26941  eldioph2b  26945  diophin  26955  eldiophss  26957  diophrex  26958  rexrabdioph  26978  eldioph4b  26997  diophren  26999  rencldnfilem  27006  irrapxlem4  27013  irrapxlem6  27015  pellex  27023  pell1234qrdich  27049  pellfundex  27074  pellfund14b  27087  jm2.26a  27196  jm2.27  27204  fnwe2lem2  27251  lsmfgcl  27275  kercvrlsm  27284  lmhmfgima  27285  lmhmfgsplit  27287  lindfrn  27394  islinds4  27408  lpirlnr  27424  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  hbtlem6  27436  hbt  27437  mpaaeu  27458  rngunsnply  27481  psgnunilem3  27522  psgnghm  27540  3cyclfrgrarn1  28435  lshpdisj  29799  cvrcon3b  30089  atnle  30129  hlhgt2  30200  hl0lt1N  30201  hl2at  30216  cvrexchlem  30230  cvratlem  30232  lvolnlelpln  30396  2lplnj  30431  ispsubcl2N  30758  lautcvr  30903  dva1dim  31796  dib1dim  31977  dib1dim2  31980  diclspsn  32006  dih1dimatlem  32141  dihlatat  32149  dihatexv  32150  dihatexv2  32151  dihjat2  32243  lcfrlem9  32362  lcfrlem16  32370  mapdrvallem2  32457  mapd1o  32460
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator