Theorem ralrimiva 2615

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
ralrimiva.1	|- ( ( ph /\ x e. A ) -> ps )

Assertion

Ref	Expression
ralrimiva	|- ( ph -> A. x e. A ps )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 |- ( ( ph /\ x e. A ) -> ps )
2	1	ex 115	. 2 |- ( ph -> ( x e. A -> ps ) )
3	2	ralrimiv 2614	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2203   A.wral 2520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525

This theorem is referenced by:  ralrimivvva  2625  rgen2  2628  rgen3  2629  nrexdv  2635  r19.29vva  2688  rabbidva  2800  ssrabdv  3316  ss2rabdv  3318  iuneq2dv  4005  iunssd  4030  disjeq2dv  4083  mpteq12dva  4184  triun  4214  issod  4431  frirrg  4462  frind  4464  peano2  4708  dmmptd  5480  fun11iun  5626  fniinfv  5726  eqfnfv  5766  eqfnfvd  5769  fnmptfvd  5773  dff3im  5813  dffo4  5816  fmptd  5822  ffnfv  5826  fmpt2d  5830  ffvresb  5831  funiun  5850  fconst2g  5890  fconstfvm  5893  resfunexg  5896  eufnfv  5908  foco2  5917  fniunfv  5926  fcofo  5948  fliftel  5957  fliftfun  5960  fliftfuns  5962  riota5f  6021  f1ocnvd  6248  suppssov1  6254  offval2  6273  ofrfval2  6274  offveqb  6277  offveq  6278  caofref  6282  caofinvl  6283  caofid0l  6284  caofid0r  6285  caofid1  6286  caofid2  6287  opabex3d  6305  uchoice  6322  oprssdmm  6356  f1od2  6422  disjxp1  6423  funsssuppss  6449  suppofss1dcl  6455  suppofss2dcl  6456  tfrlem1  6530  tfrlemisucaccv  6547  tfrlemiubacc  6552  tfr1onlemsucfn  6562  tfr1onlemsucaccv  6563  tfr1onlembxssdm  6565  tfr1onlembfn  6566  tfr1onlemubacc  6568  tfr1onlemaccex  6570  tfr1onlemres  6571  tfrcllemsucfn  6575  tfrcllemsucaccv  6576  tfrcllembxssdm  6578  tfrcllembfn  6579  tfrcllemubacc  6581  tfrcllemaccex  6583  tfrcllemres  6584  tfrcl  6586  rdgon  6608  freccllem  6624  frecfcllem  6626  omcl  6685  oeicl  6686  qliftfuns  6844  ixpeq2dva  6939  xpf1o  7088  mapxpen  7092  isinfinf  7145  fimax2gtrilemstep  7149  undifdcss  7174  opabfi  7191  fissfi  7207  2omap  7260  eqsuptid  7279  eqinftid  7303  difinfsnlem  7381  difinfsn  7382  ctmlemr  7390  ctm  7391  ctssdclemn0  7392  ctssdccl  7393  enumctlemm  7396  nninfninc  7405  nnnninf  7408  nnnninfeq  7410  enomnilem  7420  ismkvnex  7437  enmkvlem  7443  enwomnilem  7451  nninfwlporlemd  7454  nninfwlpoimlemg  7457  nninfwlpoimlemginf  7458  nninfwlpoim  7461  nninfinfwlpo  7462  finacn  7502  acfun  7505  exmidaclem  7506  exmidontriimlem4  7522  exmidontriim  7523  pw1on  7527  ccfunen  7566  cc2lem  7568  cc3  7570  acnccim  7574  genprndl  7824  genprndu  7825  nqprloc  7848  ltexprlemrnd  7908  ltexprlemdisj  7909  lteupri  7920  recexprlemrnd  7932  recexprlemdisj  7933  caucvgprlemlim  7984  caucvgprprlemlim  8014  suplocexprlemml  8019  suplocexprlemrl  8020  suplocexprlemmu  8021  suplocexprlemru  8022  suplocexprlemdisj  8023  suplocexprlemloc  8024  suplocexprlemub  8026  caucvgsrlembound  8097  caucvgsrlemgt1  8098  caucvgsrlemoffgt1  8102  caucvgsr  8105  suplocsrlemb  8109  suplocsrlempr  8110  suplocsrlem  8111  elrealeu  8132  axcaucvglemcau  8201  axcaucvglemres  8202  axpre-suploclemres  8204  negeu  8452  eqord1  8745  eqord2  8746  creur  9221  creui  9222  suprzclex  9662  supinfneg  9913  infsupneg  9914  infregelbex  9916  indstr2  9927  iooidg  10228  iccsupr  10285  icoshftf1o  10310  fznlem  10361  exfzdc  10572  zsupcllemstep  10575  infssuzex  10579  suprzubdc  10582  zsupssdc  10584  exbtwnzlemstep  10593  exbtwnzlemex  10595  frec2uzrdg  10757  frecuzrdgrcl  10758  frecuzrdgtcl  10760  frecuzrdgsuc  10762  frecuzrdgrclt  10763  frecuzrdgg  10764  frecuzrdgfunlem  10767  frecuzrdgsuctlem  10771  nninfinf  10791  iseqovex  10806  seq3val  10808  seqvalcd  10809  seq3-1  10810  seqf  10812  seq3p1  10813  seqovcd  10815  seqp1cd  10818  seq3clss  10819  seq3fveq2  10823  seqfveq2g  10825  seqfveqg  10826  seq3fveq  10827  seq3feq  10828  seq3shft2  10829  seqshft2g  10830  monoord  10833  monoord2  10834  ser3mono  10835  seq3split  10836  seqsplitg  10837  seq3caopr3  10839  seqcaopr3g  10840  seq3caopr2  10841  seqcaopr2g  10842  iseqf1olemqk  10855  iseqf1olemjpcl  10856  iseqf1olemqpcl  10857  iseqf1olemfvp  10858  seq3f1olemqsumkj  10859  seq3f1olemqsumk  10860  seq3f1olemqsum  10861  seq3f1oleml  10864  seq3f1o  10865  seqf1og  10869  seq3id3  10872  seq3id  10873  seq3id2  10874  seq3homo  10875  seq3z  10876  seqhomog  10878  seqfeq4g  10879  ser3ge0  10884  nn0ltexp2  11057  bccl  11115  hashinfuni  11125  hashennnuni  11127  wrdexg  11213  ccatlen  11261  ccatvalfn  11267  ccatrn  11275  swrdlen  11322  swrdwrdsymbg  11334  swrdswrd  11375  wrdind  11392  reuccatpfxs1  11417  shftf  11493  seq3shft  11501  caucvgrelemcau  11643  cvg1nlemcau  11647  cvg1nlemres  11648  resqrexlemcvg  11682  resqrexlemglsq  11685  resqrexlemga  11686  maxabslemval  11871  negfi  11891  minmax  11893  xrmaxiflemval  11913  xrminmax  11928  climconst  11953  2clim  11964  climcn1  11971  climcn2  11972  reccn2ap  11976  cn1lem  11977  climsqz  11998  climsqz2  11999  climcau  12010  climrecvg1n  12011  serf0  12015  sumeq2dv  12031  sumrbdclem  12041  fsum3cvg  12042  summodclem3  12044  summodclem2a  12045  zsumdc  12048  isum  12049  fsumgcl  12050  fsum3  12051  fsumf1o  12054  isumss  12055  fisumss  12056  isumss2  12057  fsum3cvg2  12058  fsumsersdc  12059  fsum3ser  12061  fsumcl2lem  12062  fsumadd  12070  fsumsplit  12071  fsumm1  12080  fsum1p  12082  isumclim3  12087  isummulc2  12090  sumsplitdc  12096  fsum2dlemstep  12098  fisumcom2  12102  fsumshftm  12109  fsummulc2  12112  fsumge1  12125  fsum00  12126  fsumabs  12129  telfsumo  12130  telfsumo2  12131  fsumparts  12134  fsumrelem  12135  fsumiun  12141  hashiun  12142  hash2iun  12143  binomlem  12147  isumshft  12154  isum1p  12156  isumnn0nn  12157  isumrpcl  12158  isumlessdc  12160  divcnv  12161  cvgratnnlemnexp  12188  cvgratnnlemmn  12189  cvgratnnlemseq  12190  cvgratnnlemabsle  12191  cvgratnnlemfm  12193  cvgratnnlemrate  12194  cvgratnn  12195  cvgratz  12196  mertenslemi1  12199  mertenslem2  12200  mertensabs  12201  clim2prod  12203  prodeq2dv  12230  prodrbdclem  12235  fproddccvg  12236  prodmodclem3  12239  prodmodclem2a  12240  zproddc  12243  iprodap  12244  fprodseq  12247  fprodf1o  12252  prodssdc  12253  fprodssdc  12254  fprodmul  12255  fprodsplit  12261  fprodm1  12262  fprod1p  12263  fprodm1s  12265  fprodp1s  12266  fprodunsn  12268  fprodcl2lem  12269  fprodabs  12280  fprodeq0  12281  fprodap0  12285  fprod2dlemstep  12286  fprodcom2fi  12290  fprodrec  12293  fprodmodd  12305  efcvgfsum  12331  dvdsssfz1  12516  bitsfi  12621  bitsinv1  12626  dvdsbnd  12630  bezoutlemstep  12671  bezoutlemmain  12672  bezoutlemle  12682  bezoutlemsup  12683  dfgcd3  12684  dfgcd2  12688  nnwodc  12710  uzwodc  12711  nnwosdc  12713  nninfctlemfo  12714  coprmgcdb  12763  prmdc  12805  isprm5  12817  isprm6  12822  phivalfi  12887  phibndlem  12891  dfphi2  12895  hashdvds  12896  phiprmpw  12897  phimullem  12900  eulerthlemfi  12903  dvdsfi  12914  hashgcdeq  12915  phisum  12916  reumodprminv  12929  pclemdc  12964  pc2dvds  13006  pcz  13008  pcprmpw2  13009  pcmptdvds  13021  pcprod  13022  pcfac  13026  qexpz  13028  prmpwdvds  13031  pockthg  13033  infpnlem2  13036  1arithlem4  13042  1arith  13043  4sqlemafi  13071  4sqlemffi  13072  4sqleminfi  13073  ennnfonelemex  13139  ennnfonelemfun  13142  ennnfonelemf1  13143  ennnfonelemnn0  13147  ennnfonelemim  13149  exmidunben  13151  ctinfomlemom  13152  ctinfom  13153  ctinf  13155  ctiunctlemudc  13162  ctiunctlemf  13163  ctiunctlemfo  13164  omctfn  13168  ssnnctlemct  13171  nninfdclemcl  13173  nninfdclemp1  13175  pwsbas  13479  imasival  13493  ismgmid2  13567  mgmidsssn0  13571  grpinvalem  13572  grpinva  13573  gsumress  13582  issgrpd  13599  prdsplusgsgrpcl  13601  sgrpidmndm  13607  ismndd  13624  mndpfo  13625  prdsplusgcl  13633  prdsidlem  13634  mhmima  13678  mhmeql  13679  gsumvallem2  13680  isgrpd2e  13707  dfgrp2  13714  grpidd2  13728  isgrpinv  13741  grplrinv  13744  grpidinv  13746  dfgrp3me  13787  prdsinvlem  13795  mhmmnd  13807  ghmgrp  13809  mulgsubcl  13827  issubg2m  13880  issubgrpd2  13881  grpissubg  13885  subgintm  13889  nmzsubg  13901  ssnmz  13902  ghmrn  13948  ghmeql  13958  ghmf1  13964  conjnmz  13970  conjnmzb  13971  rinvmod  14000  srgrz  14102  srglz  14103  srgisid  14104  ringsrg  14165  rhmdvdsr  14294  rhmopp  14295  subrngintm  14331  subrg1  14350  subrgugrp  14359  subrgintm  14362  rrgsupp  14385  unitrrg  14387  aprap  14406  islmodd  14413  lssuni  14483  lsssubg  14497  lssintclm  14504  dflidl2rng  14601  lidlsubg  14606  cnsubglem  14699  gsumfzfsumlemm  14707  znf1o  14771  znidomb  14778  psrbagfi  14794  psrbaglecl  14795  psrbagcon  14796  psr1clfi  14813  mplsubgfilemm  14823  mplsubgfilemcl  14824  mplsubgfi  14826  fiinbas  14884  tgclb  14900  restbasg  15003  iscnp4  15053  cnco  15056  cnptopco  15057  cnss1  15061  cnss2  15062  cncnpi  15063  cncnp  15065  cnconst2  15068  cnrest  15070  cnptopresti  15073  cnpdis  15077  lmtopcnp  15085  txbasval  15102  tx1cn  15104  tx2cn  15105  txcnp  15106  upxp  15107  txdis1cn  15113  cnmpt11  15118  psmet0  15162  psmettri2  15163  psmetxrge0  15167  psmetres2  15168  ismeti  15181  xmetpsmet  15204  blsscls2  15328  comet  15334  xmettx  15345  tgioo  15389  tgqioo  15390  fsumcncntop  15402  elcncf1di  15414  cdivcncfap  15439  mulcncflem  15442  mulcncf  15443  cnopnap  15446  divcncfap  15449  dedekindeulemuub  15452  dedekindeulemlu  15456  suplociccreex  15459  suplociccex  15460  dedekindicclemuub  15461  dedekindicclemlu  15465  ivthinclemlopn  15471  ivthinclemlr  15472  ivthinclemuopn  15473  ivthinclemur  15474  ivthinclemdisj  15475  ivthinclemloc  15476  ivthinc  15478  ivthdec  15479  dich0  15487  ivthdich  15488  cnplimclemr  15504  limccnp2cntop  15512  limccoap  15513  dvcn  15535  dvfre  15545  dvrecap  15548  dvmptclx  15553  dvmptaddx  15554  dvmptmulx  15555  dveflem  15561  dvef  15562  ply1termlem  15577  plyaddlem1  15582  plymullem1  15583  plycoeid3  15592  plycj  15596  plyreres  15599  dvply1  15600  sin0pilem1  15616  sin0pilem2  15617  mpodvdsmulf1o  15828  mersenne  15835  perfectlem2  15838  lgsval2lem  15853  lgsdirnn0  15890  lgsdinn0  15891  gausslemma2dlem1f1o  15903  gausslemma2dlem2  15905  gausslemma2dlem3  15906  lgsquadlemofi  15919  lgsquadlem1  15920  lgsquadlem2  15921  2lgslem1a1  15929  2sqlem6  15963  2sqlem8  15966  2sqlem10  15968  usgruspgrben  16151  uspgredg2v  16186  usgredg2v  16189  subuhgr  16237  subupgr  16238  subumgr  16239  subusgr  16240  vtxedgfi  16254  vtxlpfi  16255  wlk1walkdom  16324  wlkres  16344  eupth2lembfi  16442  depindlem1  16471  depindlem2  16472  depindlem3  16473  fnmptd  16546  bj-charfun  16547  bj-charfundc  16548  bj-charfunr  16550  pw1nct  16747  nnsf  16753  nninfalllem1  16756  nninfall  16757  nninfself  16761  nninfsellemeq  16762  nninfsellemeqinf  16764  nninfsel  16765  nnnninfex  16770  nninfnfiinf  16771  repiecef  16782  isomninnlem  16784  trilpolemeq1  16794  trilpo  16797  apdiff  16802  iswomninnlem  16804  iswomni0  16806  ismkvnnlem  16807  redcwlpo  16810  redc0  16812  reap0  16813  dceqnconst  16815  dcapnconst  16816  nconstwlpolem  16820  nconstwlpo  16821  neapmkv  16823  ltlenmkv  16825