Theorem ralrimiva 2605

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 2604	1 |- ( ph -> A. x e. A ps )

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralrimivvva  2615  rgen2  2618  rgen3  2619  nrexdv  2625  r19.29vva  2678  rabbidva  2790  ssrabdv  3306  ss2rabdv  3308  iuneq2dv  3991  iunssd  4016  disjeq2dv  4069  mpteq12dva  4170  triun  4200  issod  4416  frirrg  4447  frind  4449  peano2  4693  dmmptd  5463  fun11iun  5605  fniinfv  5705  eqfnfv  5745  eqfnfvd  5748  fnmptfvd  5752  dff3im  5793  dffo4  5796  fmptd  5802  ffnfv  5806  fmpt2d  5810  ffvresb  5811  funiun  5830  fconst2g  5870  fconstfvm  5873  resfunexg  5876  eufnfv  5888  foco2  5897  fniunfv  5906  fcofo  5928  fliftel  5937  fliftfun  5940  fliftfuns  5942  riota5f  6001  f1ocnvd  6228  suppssov1  6235  offval2  6254  ofrfval2  6255  offveqb  6258  offveq  6259  caofref  6263  caofinvl  6264  caofid0l  6265  caofid0r  6266  caofid1  6267  caofid2  6268  opabex3d  6286  uchoice  6303  oprssdmm  6337  f1od2  6403  disjxp1  6404  tfrlem1  6477  tfrlemisucaccv  6494  tfrlemiubacc  6499  tfr1onlemsucfn  6509  tfr1onlemsucaccv  6510  tfr1onlembxssdm  6512  tfr1onlembfn  6513  tfr1onlemubacc  6515  tfr1onlemaccex  6517  tfr1onlemres  6518  tfrcllemsucfn  6522  tfrcllemsucaccv  6523  tfrcllembxssdm  6525  tfrcllembfn  6526  tfrcllemubacc  6528  tfrcllemaccex  6530  tfrcllemres  6531  tfrcl  6533  rdgon  6555  freccllem  6571  frecfcllem  6573  omcl  6632  oeicl  6633  qliftfuns  6791  ixpeq2dva  6885  xpf1o  7033  mapxpen  7037  isinfinf  7089  fimax2gtrilemstep  7093  undifdcss  7118  opabfi  7135  eqsuptid  7199  eqinftid  7223  difinfsnlem  7301  difinfsn  7302  ctmlemr  7310  ctm  7311  ctssdclemn0  7312  ctssdccl  7313  enumctlemm  7316  nninfninc  7325  nnnninf  7328  nnnninfeq  7330  enomnilem  7340  ismkvnex  7357  enmkvlem  7363  enwomnilem  7371  nninfwlporlemd  7374  nninfwlpoimlemg  7377  nninfwlpoimlemginf  7378  nninfwlpoim  7381  nninfinfwlpo  7382  finacn  7422  acfun  7425  exmidaclem  7426  exmidontriimlem4  7442  exmidontriim  7443  pw1on  7447  ccfunen  7486  cc2lem  7488  cc3  7490  acnccim  7494  genprndl  7744  genprndu  7745  nqprloc  7768  ltexprlemrnd  7828  ltexprlemdisj  7829  lteupri  7840  recexprlemrnd  7852  recexprlemdisj  7853  caucvgprlemlim  7904  caucvgprprlemlim  7934  suplocexprlemml  7939  suplocexprlemrl  7940  suplocexprlemmu  7941  suplocexprlemru  7942  suplocexprlemdisj  7943  suplocexprlemloc  7944  suplocexprlemub  7946  caucvgsrlembound  8017  caucvgsrlemgt1  8018  caucvgsrlemoffgt1  8022  caucvgsr  8025  suplocsrlemb  8029  suplocsrlempr  8030  suplocsrlem  8031  elrealeu  8052  axcaucvglemcau  8121  axcaucvglemres  8122  axpre-suploclemres  8124  negeu  8373  eqord1  8666  eqord2  8667  creur  9142  creui  9143  suprzclex  9581  supinfneg  9832  infsupneg  9833  infregelbex  9835  indstr2  9846  iooidg  10147  iccsupr  10204  icoshftf1o  10229  fznlem  10279  exfzdc  10490  zsupcllemstep  10493  infssuzex  10497  suprzubdc  10500  zsupssdc  10502  exbtwnzlemstep  10511  exbtwnzlemex  10513  frec2uzrdg  10675  frecuzrdgrcl  10676  frecuzrdgtcl  10678  frecuzrdgsuc  10680  frecuzrdgrclt  10681  frecuzrdgg  10682  frecuzrdgfunlem  10685  frecuzrdgsuctlem  10689  nninfinf  10709  iseqovex  10724  seq3val  10726  seqvalcd  10727  seq3-1  10728  seqf  10730  seq3p1  10731  seqovcd  10733  seqp1cd  10736  seq3clss  10737  seq3fveq2  10741  seqfveq2g  10743  seqfveqg  10744  seq3fveq  10745  seq3feq  10746  seq3shft2  10747  seqshft2g  10748  monoord  10751  monoord2  10752  ser3mono  10753  seq3split  10754  seqsplitg  10755  seq3caopr3  10757  seqcaopr3g  10758  seq3caopr2  10759  seqcaopr2g  10760  iseqf1olemqk  10773  iseqf1olemjpcl  10774  iseqf1olemqpcl  10775  iseqf1olemfvp  10776  seq3f1olemqsumkj  10777  seq3f1olemqsumk  10778  seq3f1olemqsum  10779  seq3f1oleml  10782  seq3f1o  10783  seqf1og  10787  seq3id3  10790  seq3id  10791  seq3id2  10792  seq3homo  10793  seq3z  10794  seqhomog  10796  seqfeq4g  10797  ser3ge0  10802  nn0ltexp2  10975  bccl  11033  hashinfuni  11043  hashennnuni  11045  wrdexg  11131  ccatlen  11179  ccatvalfn  11185  ccatrn  11193  swrdlen  11240  swrdwrdsymbg  11252  swrdswrd  11293  wrdind  11310  reuccatpfxs1  11335  shftf  11411  seq3shft  11419  caucvgrelemcau  11561  cvg1nlemcau  11565  cvg1nlemres  11566  resqrexlemcvg  11600  resqrexlemglsq  11603  resqrexlemga  11604  maxabslemval  11789  negfi  11809  minmax  11811  xrmaxiflemval  11831  xrminmax  11846  climconst  11871  2clim  11882  climcn1  11889  climcn2  11890  reccn2ap  11894  cn1lem  11895  climsqz  11916  climsqz2  11917  climcau  11928  climrecvg1n  11929  serf0  11933  sumeq2dv  11949  sumrbdclem  11959  fsum3cvg  11960  summodclem3  11962  summodclem2a  11963  zsumdc  11966  isum  11967  fsumgcl  11968  fsum3  11969  fsumf1o  11972  isumss  11973  fisumss  11974  isumss2  11975  fsum3cvg2  11976  fsumsersdc  11977  fsum3ser  11979  fsumcl2lem  11980  fsumadd  11988  fsumsplit  11989  fsumm1  11998  fsum1p  12000  isumclim3  12005  isummulc2  12008  sumsplitdc  12014  fsum2dlemstep  12016  fisumcom2  12020  fsumshftm  12027  fsummulc2  12030  fsumge1  12043  fsum00  12044  fsumabs  12047  telfsumo  12048  telfsumo2  12049  fsumparts  12052  fsumrelem  12053  fsumiun  12059  hashiun  12060  hash2iun  12061  binomlem  12065  isumshft  12072  isum1p  12074  isumnn0nn  12075  isumrpcl  12076  isumlessdc  12078  divcnv  12079  cvgratnnlemnexp  12106  cvgratnnlemmn  12107  cvgratnnlemseq  12108  cvgratnnlemabsle  12109  cvgratnnlemfm  12111  cvgratnnlemrate  12112  cvgratnn  12113  cvgratz  12114  mertenslemi1  12117  mertenslem2  12118  mertensabs  12119  clim2prod  12121  prodeq2dv  12148  prodrbdclem  12153  fproddccvg  12154  prodmodclem3  12157  prodmodclem2a  12158  zproddc  12161  iprodap  12162  fprodseq  12165  fprodf1o  12170  prodssdc  12171  fprodssdc  12172  fprodmul  12173  fprodsplit  12179  fprodm1  12180  fprod1p  12181  fprodm1s  12183  fprodp1s  12184  fprodunsn  12186  fprodcl2lem  12187  fprodabs  12198  fprodeq0  12199  fprodap0  12203  fprod2dlemstep  12204  fprodcom2fi  12208  fprodrec  12211  fprodmodd  12223  efcvgfsum  12249  dvdsssfz1  12434  bitsfi  12539  bitsinv1  12544  dvdsbnd  12548  bezoutlemstep  12589  bezoutlemmain  12590  bezoutlemle  12600  bezoutlemsup  12601  dfgcd3  12602  dfgcd2  12606  nnwodc  12628  uzwodc  12629  nnwosdc  12631  nninfctlemfo  12632  coprmgcdb  12681  prmdc  12723  isprm5  12735  isprm6  12740  phivalfi  12805  phibndlem  12809  dfphi2  12813  hashdvds  12814  phiprmpw  12815  phimullem  12818  eulerthlemfi  12821  dvdsfi  12832  hashgcdeq  12833  phisum  12834  reumodprminv  12847  pclemdc  12882  pc2dvds  12924  pcz  12926  pcprmpw2  12927  pcmptdvds  12939  pcprod  12940  pcfac  12944  qexpz  12946  prmpwdvds  12949  pockthg  12951  infpnlem2  12954  1arithlem4  12960  1arith  12961  4sqlemafi  12989  4sqlemffi  12990  4sqleminfi  12991  ennnfonelemex  13056  ennnfonelemfun  13059  ennnfonelemf1  13060  ennnfonelemnn0  13064  ennnfonelemim  13066  exmidunben  13068  ctinfomlemom  13069  ctinfom  13070  ctinf  13072  ctiunctlemudc  13079  ctiunctlemf  13080  ctiunctlemfo  13081  omctfn  13085  ssnnctlemct  13088  nninfdclemcl  13090  nninfdclemp1  13092  pwsbas  13396  imasival  13410  ismgmid2  13484  mgmidsssn0  13488  grpinvalem  13489  grpinva  13490  gsumress  13499  issgrpd  13516  prdsplusgsgrpcl  13518  sgrpidmndm  13524  ismndd  13541  mndpfo  13542  prdsplusgcl  13550  prdsidlem  13551  mhmima  13595  mhmeql  13596  gsumvallem2  13597  isgrpd2e  13624  dfgrp2  13631  grpidd2  13645  isgrpinv  13658  grplrinv  13661  grpidinv  13663  dfgrp3me  13704  prdsinvlem  13712  mhmmnd  13724  ghmgrp  13726  mulgsubcl  13744  issubg2m  13797  issubgrpd2  13798  grpissubg  13802  subgintm  13806  nmzsubg  13818  ssnmz  13819  ghmrn  13865  ghmeql  13875  ghmf1  13881  conjnmz  13887  conjnmzb  13888  rinvmod  13917  srgrz  14019  srglz  14020  srgisid  14021  ringsrg  14082  rhmdvdsr  14211  rhmopp  14212  subrngintm  14248  subrg1  14267  subrgugrp  14276  subrgintm  14279  unitrrg  14303  aprap  14322  islmodd  14329  lssuni  14399  lsssubg  14413  lssintclm  14420  dflidl2rng  14517  lidlsubg  14522  cnsubglem  14615  gsumfzfsumlemm  14623  znf1o  14687  znidomb  14694  psrbagfi  14710  psrbaglecl  14711  psrbagcon  14712  psr1clfi  14729  mplsubgfilemm  14739  mplsubgfilemcl  14740  mplsubgfi  14742  fiinbas  14800  tgclb  14816  restbasg  14919  iscnp4  14969  cnco  14972  cnptopco  14973  cnss1  14977  cnss2  14978  cncnpi  14979  cncnp  14981  cnconst2  14984  cnrest  14986  cnptopresti  14989  cnpdis  14993  lmtopcnp  15001  txbasval  15018  tx1cn  15020  tx2cn  15021  txcnp  15022  upxp  15023  txdis1cn  15029  cnmpt11  15034  psmet0  15078  psmettri2  15079  psmetxrge0  15083  psmetres2  15084  ismeti  15097  xmetpsmet  15120  blsscls2  15244  comet  15250  xmettx  15261  tgioo  15305  tgqioo  15306  fsumcncntop  15318  elcncf1di  15330  cdivcncfap  15355  mulcncflem  15358  mulcncf  15359  cnopnap  15362  divcncfap  15365  dedekindeulemuub  15368  dedekindeulemlu  15372  suplociccreex  15375  suplociccex  15376  dedekindicclemuub  15377  dedekindicclemlu  15381  ivthinclemlopn  15387  ivthinclemlr  15388  ivthinclemuopn  15389  ivthinclemur  15390  ivthinclemdisj  15391  ivthinclemloc  15392  ivthinc  15394  ivthdec  15395  dich0  15403  ivthdich  15404  cnplimclemr  15420  limccnp2cntop  15428  limccoap  15429  dvcn  15451  dvfre  15461  dvrecap  15464  dvmptclx  15469  dvmptaddx  15470  dvmptmulx  15471  dveflem  15477  dvef  15478  ply1termlem  15493  plyaddlem1  15498  plymullem1  15499  plycoeid3  15508  plycj  15512  plyreres  15515  dvply1  15516  sin0pilem1  15532  sin0pilem2  15533  mpodvdsmulf1o  15741  mersenne  15748  perfectlem2  15751  lgsval2lem  15766  lgsdirnn0  15803  lgsdinn0  15804  gausslemma2dlem1f1o  15816  gausslemma2dlem2  15818  gausslemma2dlem3  15819  lgsquadlemofi  15832  lgsquadlem1  15833  lgsquadlem2  15834  2lgslem1a1  15842  2sqlem6  15876  2sqlem8  15879  2sqlem10  15881  usgruspgrben  16064  uspgredg2v  16099  usgredg2v  16102  subuhgr  16150  subupgr  16151  subumgr  16152  subusgr  16153  vtxedgfi  16167  vtxlpfi  16168  wlk1walkdom  16237  wlkres  16257  eupth2lembfi  16355  depindlem1  16384  depindlem2  16385  depindlem3  16386  fnmptd  16459  bj-charfun  16461  bj-charfundc  16462  bj-charfunr  16464  2omap  16653  pw1nct  16663  nnsf  16666  nninfalllem1  16669  nninfall  16670  nninfself  16674  nninfsellemeq  16675  nninfsellemeqinf  16677  nninfsel  16678  nnnninfex  16683  nninfnfiinf  16684  isomninnlem  16693  trilpolemeq1  16703  trilpo  16706  apdiff  16711  iswomninnlem  16713  iswomni0  16715  ismkvnnlem  16716  redcwlpo  16719  redc0  16721  reap0  16722  dceqnconst  16724  dcapnconst  16725  nconstwlpolem  16729  nconstwlpo  16730  neapmkv  16732  ltlenmkv  16734