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  5604  fniinfv  5704  eqfnfv  5744  eqfnfvd  5747  fnmptfvd  5751  dff3im  5792  dffo4  5795  fmptd  5801  ffnfv  5805  fmpt2d  5809  ffvresb  5810  funiun  5829  fconst2g  5869  fconstfvm  5872  resfunexg  5875  eufnfv  5885  foco2  5894  fniunfv  5903  fcofo  5925  fliftel  5934  fliftfun  5937  fliftfuns  5939  riota5f  5998  f1ocnvd  6225  suppssov1  6232  offval2  6251  ofrfval2  6252  offveqb  6255  offveq  6256  caofref  6260  caofinvl  6261  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  opabex3d  6283  uchoice  6300  oprssdmm  6334  f1od2  6400  disjxp1  6401  tfrlem1  6474  tfrlemisucaccv  6491  tfrlemiubacc  6496  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  rdgon  6552  freccllem  6568  frecfcllem  6570  omcl  6629  oeicl  6630  qliftfuns  6788  ixpeq2dva  6882  xpf1o  7030  mapxpen  7034  isinfinf  7086  fimax2gtrilemstep  7090  undifdcss  7115  opabfi  7132  eqsuptid  7196  eqinftid  7220  difinfsnlem  7298  difinfsn  7299  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  enumctlemm  7313  nninfninc  7322  nnnninf  7325  nnnninfeq  7327  enomnilem  7337  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  nninfwlporlemd  7371  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  finacn  7419  acfun  7422  exmidaclem  7423  exmidontriimlem4  7439  exmidontriim  7440  pw1on  7444  ccfunen  7483  cc2lem  7485  cc3  7487  acnccim  7491  genprndl  7741  genprndu  7742  nqprloc  7765  ltexprlemrnd  7825  ltexprlemdisj  7826  lteupri  7837  recexprlemrnd  7849  recexprlemdisj  7850  caucvgprlemlim  7901  caucvgprprlemlim  7931  suplocexprlemml  7936  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  caucvgsrlembound  8014  caucvgsrlemgt1  8015  caucvgsrlemoffgt1  8019  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  elrealeu  8049  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  negeu  8370  eqord1  8663  eqord2  8664  creur  9139  creui  9140  suprzclex  9578  supinfneg  9829  infsupneg  9830  infregelbex  9832  indstr2  9843  iooidg  10144  iccsupr  10201  icoshftf1o  10226  fznlem  10276  exfzdc  10486  zsupcllemstep  10489  infssuzex  10493  suprzubdc  10496  zsupssdc  10498  exbtwnzlemstep  10507  exbtwnzlemex  10509  frec2uzrdg  10671  frecuzrdgrcl  10672  frecuzrdgtcl  10674  frecuzrdgsuc  10676  frecuzrdgrclt  10677  frecuzrdgg  10678  frecuzrdgfunlem  10681  frecuzrdgsuctlem  10685  nninfinf  10705  iseqovex  10720  seq3val  10722  seqvalcd  10723  seq3-1  10724  seqf  10726  seq3p1  10727  seqovcd  10729  seqp1cd  10732  seq3clss  10733  seq3fveq2  10737  seqfveq2g  10739  seqfveqg  10740  seq3fveq  10741  seq3feq  10742  seq3shft2  10743  seqshft2g  10744  monoord  10747  monoord2  10748  ser3mono  10749  seq3split  10750  seqsplitg  10751  seq3caopr3  10753  seqcaopr3g  10754  seq3caopr2  10755  seqcaopr2g  10756  iseqf1olemqk  10769  iseqf1olemjpcl  10770  iseqf1olemqpcl  10771  iseqf1olemfvp  10772  seq3f1olemqsumkj  10773  seq3f1olemqsumk  10774  seq3f1olemqsum  10775  seq3f1oleml  10778  seq3f1o  10779  seqf1og  10783  seq3id3  10786  seq3id  10787  seq3id2  10788  seq3homo  10789  seq3z  10790  seqhomog  10792  seqfeq4g  10793  ser3ge0  10798  nn0ltexp2  10971  bccl  11029  hashinfuni  11039  hashennnuni  11041  wrdexg  11124  ccatlen  11172  ccatvalfn  11178  ccatrn  11186  swrdlen  11233  swrdwrdsymbg  11245  swrdswrd  11286  wrdind  11303  reuccatpfxs1  11328  shftf  11391  seq3shft  11399  caucvgrelemcau  11541  cvg1nlemcau  11545  cvg1nlemres  11546  resqrexlemcvg  11580  resqrexlemglsq  11583  resqrexlemga  11584  maxabslemval  11769  negfi  11789  minmax  11791  xrmaxiflemval  11811  xrminmax  11826  climconst  11851  2clim  11862  climcn1  11869  climcn2  11870  reccn2ap  11874  cn1lem  11875  climsqz  11896  climsqz2  11897  climcau  11908  climrecvg1n  11909  serf0  11913  sumeq2dv  11929  sumrbdclem  11939  fsum3cvg  11940  summodclem3  11942  summodclem2a  11943  zsumdc  11946  isum  11947  fsumgcl  11948  fsum3  11949  fsumf1o  11952  isumss  11953  fisumss  11954  isumss2  11955  fsum3cvg2  11956  fsumsersdc  11957  fsum3ser  11959  fsumcl2lem  11960  fsumadd  11968  fsumsplit  11969  fsumm1  11978  fsum1p  11980  isumclim3  11985  isummulc2  11988  sumsplitdc  11994  fsum2dlemstep  11996  fisumcom2  12000  fsumshftm  12007  fsummulc2  12010  fsumge1  12023  fsum00  12024  fsumabs  12027  telfsumo  12028  telfsumo2  12029  fsumparts  12032  fsumrelem  12033  fsumiun  12039  hashiun  12040  hash2iun  12041  binomlem  12045  isumshft  12052  isum1p  12054  isumnn0nn  12055  isumrpcl  12056  isumlessdc  12058  divcnv  12059  cvgratnnlemnexp  12086  cvgratnnlemmn  12087  cvgratnnlemseq  12088  cvgratnnlemabsle  12089  cvgratnnlemfm  12091  cvgratnnlemrate  12092  cvgratnn  12093  cvgratz  12094  mertenslemi1  12097  mertenslem2  12098  mertensabs  12099  clim2prod  12101  prodeq2dv  12128  prodrbdclem  12133  fproddccvg  12134  prodmodclem3  12137  prodmodclem2a  12138  zproddc  12141  iprodap  12142  fprodseq  12145  fprodf1o  12150  prodssdc  12151  fprodssdc  12152  fprodmul  12153  fprodsplit  12159  fprodm1  12160  fprod1p  12161  fprodm1s  12163  fprodp1s  12164  fprodunsn  12166  fprodcl2lem  12167  fprodabs  12178  fprodeq0  12179  fprodap0  12183  fprod2dlemstep  12184  fprodcom2fi  12188  fprodrec  12191  fprodmodd  12203  efcvgfsum  12229  dvdsssfz1  12414  bitsfi  12519  bitsinv1  12524  dvdsbnd  12528  bezoutlemstep  12569  bezoutlemmain  12570  bezoutlemle  12580  bezoutlemsup  12581  dfgcd3  12582  dfgcd2  12586  nnwodc  12608  uzwodc  12609  nnwosdc  12611  nninfctlemfo  12612  coprmgcdb  12661  prmdc  12703  isprm5  12715  isprm6  12720  phivalfi  12785  phibndlem  12789  dfphi2  12793  hashdvds  12794  phiprmpw  12795  phimullem  12798  eulerthlemfi  12801  dvdsfi  12812  hashgcdeq  12813  phisum  12814  reumodprminv  12827  pclemdc  12862  pc2dvds  12904  pcz  12906  pcprmpw2  12907  pcmptdvds  12919  pcprod  12920  pcfac  12924  qexpz  12926  prmpwdvds  12929  pockthg  12931  infpnlem2  12934  1arithlem4  12940  1arith  12941  4sqlemafi  12969  4sqlemffi  12970  4sqleminfi  12971  ennnfonelemex  13036  ennnfonelemfun  13039  ennnfonelemf1  13040  ennnfonelemnn0  13044  ennnfonelemim  13046  exmidunben  13048  ctinfomlemom  13049  ctinfom  13050  ctinf  13052  ctiunctlemudc  13059  ctiunctlemf  13060  ctiunctlemfo  13061  omctfn  13065  ssnnctlemct  13068  nninfdclemcl  13070  nninfdclemp1  13072  pwsbas  13376  imasival  13390  ismgmid2  13464  mgmidsssn0  13468  grpinvalem  13469  grpinva  13470  gsumress  13479  issgrpd  13496  prdsplusgsgrpcl  13498  sgrpidmndm  13504  ismndd  13521  mndpfo  13522  prdsplusgcl  13530  prdsidlem  13531  mhmima  13575  mhmeql  13576  gsumvallem2  13577  isgrpd2e  13604  dfgrp2  13611  grpidd2  13625  isgrpinv  13638  grplrinv  13641  grpidinv  13643  dfgrp3me  13684  prdsinvlem  13692  mhmmnd  13704  ghmgrp  13706  mulgsubcl  13724  issubg2m  13777  issubgrpd2  13778  grpissubg  13782  subgintm  13786  nmzsubg  13798  ssnmz  13799  ghmrn  13845  ghmeql  13855  ghmf1  13861  conjnmz  13867  conjnmzb  13868  rinvmod  13897  srgrz  13999  srglz  14000  srgisid  14001  ringsrg  14062  rhmdvdsr  14191  rhmopp  14192  subrngintm  14228  subrg1  14247  subrgugrp  14256  subrgintm  14259  unitrrg  14283  aprap  14302  islmodd  14309  lssuni  14379  lsssubg  14393  lssintclm  14400  dflidl2rng  14497  lidlsubg  14502  cnsubglem  14595  gsumfzfsumlemm  14603  znf1o  14667  znidomb  14674  psrbagfi  14689  psr1clfi  14704  mplsubgfilemm  14714  mplsubgfilemcl  14715  mplsubgfi  14717  fiinbas  14775  tgclb  14791  restbasg  14894  iscnp4  14944  cnco  14947  cnptopco  14948  cnss1  14952  cnss2  14953  cncnpi  14954  cncnp  14956  cnconst2  14959  cnrest  14961  cnptopresti  14964  cnpdis  14968  lmtopcnp  14976  txbasval  14993  tx1cn  14995  tx2cn  14996  txcnp  14997  upxp  14998  txdis1cn  15004  cnmpt11  15009  psmet0  15053  psmettri2  15054  psmetxrge0  15058  psmetres2  15059  ismeti  15072  xmetpsmet  15095  blsscls2  15219  comet  15225  xmettx  15236  tgioo  15280  tgqioo  15281  fsumcncntop  15293  elcncf1di  15305  cdivcncfap  15330  mulcncflem  15333  mulcncf  15334  cnopnap  15337  divcncfap  15340  dedekindeulemuub  15343  dedekindeulemlu  15347  suplociccreex  15350  suplociccex  15351  dedekindicclemuub  15352  dedekindicclemlu  15356  ivthinclemlopn  15362  ivthinclemlr  15363  ivthinclemuopn  15364  ivthinclemur  15365  ivthinclemdisj  15366  ivthinclemloc  15367  ivthinc  15369  ivthdec  15370  dich0  15378  ivthdich  15379  cnplimclemr  15395  limccnp2cntop  15403  limccoap  15404  dvcn  15426  dvfre  15436  dvrecap  15439  dvmptclx  15444  dvmptaddx  15445  dvmptmulx  15446  dveflem  15452  dvef  15453  ply1termlem  15468  plyaddlem1  15473  plymullem1  15474  plycoeid3  15483  plycj  15487  plyreres  15490  dvply1  15491  sin0pilem1  15507  sin0pilem2  15508  mpodvdsmulf1o  15716  mersenne  15723  perfectlem2  15726  lgsval2lem  15741  lgsdirnn0  15778  lgsdinn0  15779  gausslemma2dlem1f1o  15791  gausslemma2dlem2  15793  gausslemma2dlem3  15794  lgsquadlemofi  15807  lgsquadlem1  15808  lgsquadlem2  15809  2lgslem1a1  15817  2sqlem6  15851  2sqlem8  15854  2sqlem10  15856  usgruspgrben  16039  uspgredg2v  16074  usgredg2v  16077  subuhgr  16125  subupgr  16126  subumgr  16127  subusgr  16128  vtxedgfi  16142  vtxlpfi  16143  wlk1walkdom  16212  wlkres  16232  fnmptd  16403  bj-charfun  16405  bj-charfundc  16406  bj-charfunr  16408  2omap  16597  pw1nct  16607  nnsf  16610  nninfalllem1  16613  nninfall  16614  nninfself  16618  nninfsellemeq  16619  nninfsellemeqinf  16621  nninfsel  16622  nnnninfex  16627  nninfnfiinf  16628  isomninnlem  16637  trilpolemeq1  16647  trilpo  16650  apdiff  16655  iswomninnlem  16656  iswomni0  16658  ismkvnnlem  16659  redcwlpo  16662  redc0  16664  reap0  16665  dceqnconst  16667  dcapnconst  16668  nconstwlpolem  16672  nconstwlpo  16673  neapmkv  16675  ltlenmkv  16677