Theorem ralrimiva 2570

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralrimivvva  2580  rgen2  2583  rgen3  2584  nrexdv  2590  r19.29vva  2642  rabbidva  2751  ssrabdv  3262  ss2rabdv  3264  iuneq2dv  3937  iunssd  3962  disjeq2dv  4015  mpteq12dva  4114  triun  4144  issod  4354  frirrg  4385  frind  4387  peano2  4631  dmmptd  5388  fun11iun  5525  fniinfv  5619  eqfnfv  5659  eqfnfvd  5662  fnmptfvd  5666  dff3im  5707  dffo4  5710  fmptd  5716  ffnfv  5720  fmpt2d  5724  ffvresb  5725  fconst2g  5777  fconstfvm  5780  resfunexg  5783  eufnfv  5793  foco2  5800  fniunfv  5809  fcofo  5831  fliftel  5840  fliftfun  5843  fliftfuns  5845  riota5f  5902  f1ocnvd  6125  suppssov1  6132  offval2  6151  ofrfval2  6152  offveqb  6155  caofref  6159  caofinvl  6160  opabex3d  6178  uchoice  6195  oprssdmm  6229  f1od2  6293  disjxp1  6294  tfrlem1  6366  tfrlemisucaccv  6383  tfrlemiubacc  6388  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemubacc  6404  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemubacc  6417  tfrcllemaccex  6419  tfrcllemres  6420  tfrcl  6422  rdgon  6444  freccllem  6460  frecfcllem  6462  omcl  6519  oeicl  6520  qliftfuns  6678  ixpeq2dva  6772  xpf1o  6905  mapxpen  6909  isinfinf  6958  fimax2gtrilemstep  6961  undifdcss  6984  opabfi  6999  eqsuptid  7063  eqinftid  7087  difinfsnlem  7165  difinfsn  7166  ctmlemr  7174  ctm  7175  ctssdclemn0  7176  ctssdccl  7177  enumctlemm  7180  nninfninc  7189  nnnninf  7192  nnnninfeq  7194  enomnilem  7204  ismkvnex  7221  enmkvlem  7227  enwomnilem  7235  nninfwlporlemd  7238  nninfwlpoimlemg  7241  nninfwlpoimlemginf  7242  nninfwlpoim  7244  acfun  7274  exmidaclem  7275  exmidontriimlem4  7291  exmidontriim  7292  pw1on  7293  ccfunen  7331  cc2lem  7333  cc3  7335  genprndl  7588  genprndu  7589  nqprloc  7612  ltexprlemrnd  7672  ltexprlemdisj  7673  lteupri  7684  recexprlemrnd  7696  recexprlemdisj  7697  caucvgprlemlim  7748  caucvgprprlemlim  7778  suplocexprlemml  7783  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  caucvgsrlembound  7861  caucvgsrlemgt1  7862  caucvgsrlemoffgt1  7866  caucvgsr  7869  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  elrealeu  7896  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  negeu  8217  eqord1  8510  eqord2  8511  creur  8986  creui  8987  suprzclex  9424  supinfneg  9669  infsupneg  9670  infregelbex  9672  indstr2  9683  iooidg  9984  iccsupr  10041  icoshftf1o  10066  fznlem  10116  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  suprzubdc  10326  zsupssdc  10328  exbtwnzlemstep  10337  exbtwnzlemex  10339  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgtcl  10504  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  frecuzrdgfunlem  10511  frecuzrdgsuctlem  10515  nninfinf  10535  iseqovex  10550  seq3val  10552  seqvalcd  10553  seq3-1  10554  seqf  10556  seq3p1  10557  seqovcd  10559  seqp1cd  10562  seq3clss  10563  seq3fveq2  10567  seqfveq2g  10569  seqfveqg  10570  seq3fveq  10571  seq3feq  10572  seq3shft2  10573  seqshft2g  10574  monoord  10577  monoord2  10578  ser3mono  10579  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemqk  10599  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1oleml  10608  seq3f1o  10609  seqf1og  10613  seq3id3  10616  seq3id  10617  seq3id2  10618  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  ser3ge0  10628  nn0ltexp2  10801  bccl  10859  hashinfuni  10869  hashennnuni  10871  wrdexg  10946  shftf  10995  seq3shft  11003  caucvgrelemcau  11145  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemcvg  11184  resqrexlemglsq  11187  resqrexlemga  11188  maxabslemval  11373  negfi  11393  minmax  11395  xrmaxiflemval  11415  xrminmax  11430  climconst  11455  2clim  11466  climcn1  11473  climcn2  11474  reccn2ap  11478  cn1lem  11479  climsqz  11500  climsqz2  11501  climcau  11512  climrecvg1n  11513  serf0  11517  sumeq2dv  11533  sumrbdclem  11542  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  zsumdc  11549  isum  11550  fsumgcl  11551  fsum3  11552  fsumf1o  11555  isumss  11556  fisumss  11557  isumss2  11558  fsum3cvg2  11559  fsumsersdc  11560  fsum3ser  11562  fsumcl2lem  11563  fsumadd  11571  fsumsplit  11572  fsumm1  11581  fsum1p  11583  isumclim3  11588  isummulc2  11591  sumsplitdc  11597  fsum2dlemstep  11599  fisumcom2  11603  fsumshftm  11610  fsummulc2  11613  fsumge1  11626  fsum00  11627  fsumabs  11630  telfsumo  11631  telfsumo2  11632  fsumparts  11635  fsumrelem  11636  fsumiun  11642  hashiun  11643  hash2iun  11644  binomlem  11648  isumshft  11655  isum1p  11657  isumnn0nn  11658  isumrpcl  11659  isumlessdc  11661  divcnv  11662  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemseq  11691  cvgratnnlemabsle  11692  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratnn  11696  cvgratz  11697  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  clim2prod  11704  prodeq2dv  11731  prodrbdclem  11736  fproddccvg  11737  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  iprodap  11745  fprodseq  11748  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodmul  11756  fprodsplit  11762  fprodm1  11763  fprod1p  11764  fprodm1s  11766  fprodp1s  11767  fprodunsn  11769  fprodcl2lem  11770  fprodabs  11781  fprodeq0  11782  fprodap0  11786  fprod2dlemstep  11787  fprodcom2fi  11791  fprodrec  11794  fprodmodd  11806  efcvgfsum  11832  dvdsssfz1  12017  dvdsbnd  12123  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemle  12175  bezoutlemsup  12176  dfgcd3  12177  dfgcd2  12181  nnwodc  12203  uzwodc  12204  nnwosdc  12206  nninfctlemfo  12207  coprmgcdb  12256  prmdc  12298  isprm5  12310  isprm6  12315  phivalfi  12380  phibndlem  12384  dfphi2  12388  hashdvds  12389  phiprmpw  12390  phimullem  12393  eulerthlemfi  12396  dvdsfi  12407  hashgcdeq  12408  phisum  12409  reumodprminv  12422  pclemdc  12457  pc2dvds  12499  pcz  12501  pcprmpw2  12502  pcmptdvds  12514  pcprod  12515  pcfac  12519  qexpz  12521  prmpwdvds  12524  pockthg  12526  infpnlem2  12529  1arithlem4  12535  1arith  12536  4sqlemafi  12564  4sqlemffi  12565  4sqleminfi  12566  ennnfonelemex  12631  ennnfonelemfun  12634  ennnfonelemf1  12635  ennnfonelemnn0  12639  ennnfonelemim  12641  exmidunben  12643  ctinfomlemom  12644  ctinfom  12645  ctinf  12647  ctiunctlemudc  12654  ctiunctlemf  12655  ctiunctlemfo  12656  omctfn  12660  ssnnctlemct  12663  nninfdclemcl  12665  nninfdclemp1  12667  imasival  12949  ismgmid2  13023  mgmidsssn0  13027  grpinvalem  13028  grpinva  13029  gsumress  13038  issgrpd  13055  sgrpidmndm  13061  ismndd  13078  mndpfo  13079  mhmima  13123  mhmeql  13124  gsumvallem2  13125  isgrpd2e  13152  dfgrp2  13159  grpidd2  13173  isgrpinv  13186  grplrinv  13189  grpidinv  13191  dfgrp3me  13232  mhmmnd  13246  ghmgrp  13248  mulgsubcl  13266  issubg2m  13319  issubgrpd2  13320  grpissubg  13324  subgintm  13328  nmzsubg  13340  ssnmz  13341  ghmrn  13387  ghmeql  13397  ghmf1  13403  conjnmz  13409  conjnmzb  13410  rinvmod  13439  srgrz  13540  srglz  13541  srgisid  13542  ringsrg  13603  rhmdvdsr  13731  rhmopp  13732  subrngintm  13768  subrg1  13787  subrgugrp  13796  subrgintm  13799  unitrrg  13823  aprap  13842  islmodd  13849  lssuni  13919  lsssubg  13933  lssintclm  13940  dflidl2rng  14037  lidlsubg  14042  cnsubglem  14135  gsumfzfsumlemm  14143  znf1o  14207  znidomb  14214  fiinbas  14285  tgclb  14301  restbasg  14404  iscnp4  14454  cnco  14457  cnptopco  14458  cnss1  14462  cnss2  14463  cncnpi  14464  cncnp  14466  cnconst2  14469  cnrest  14471  cnptopresti  14474  cnpdis  14478  lmtopcnp  14486  txbasval  14503  tx1cn  14505  tx2cn  14506  txcnp  14507  upxp  14508  txdis1cn  14514  cnmpt11  14519  psmet0  14563  psmettri2  14564  psmetxrge0  14568  psmetres2  14569  ismeti  14582  xmetpsmet  14605  blsscls2  14729  comet  14735  xmettx  14746  tgioo  14790  tgqioo  14791  fsumcncntop  14803  elcncf1di  14815  cdivcncfap  14840  mulcncflem  14843  mulcncf  14844  cnopnap  14847  divcncfap  14850  dedekindeulemuub  14853  dedekindeulemlu  14857  suplociccreex  14860  suplociccex  14861  dedekindicclemuub  14862  dedekindicclemlu  14866  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemdisj  14876  ivthinclemloc  14877  ivthinc  14879  ivthdec  14880  dich0  14888  ivthdich  14889  cnplimclemr  14905  limccnp2cntop  14913  limccoap  14914  dvcn  14936  dvfre  14946  dvrecap  14949  dvmptclx  14954  dvmptaddx  14955  dvmptmulx  14956  dveflem  14962  dvef  14963  ply1termlem  14978  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  plycj  14997  plyreres  15000  dvply1  15001  sin0pilem1  15017  sin0pilem2  15018  mpodvdsmulf1o  15226  mersenne  15233  perfectlem2  15236  lgsval2lem  15251  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1f1o  15301  gausslemma2dlem2  15303  gausslemma2dlem3  15304  lgsquadlemofi  15317  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1a1  15327  2sqlem6  15361  2sqlem8  15364  2sqlem10  15366  fnmptd  15450  bj-charfun  15453  bj-charfundc  15454  bj-charfunr  15456  pw1nct  15647  nnsf  15649  nninfalllem1  15652  nninfall  15653  nninfself  15657  nninfsellemeq  15658  nninfsellemeqinf  15660  nninfsel  15661  isomninnlem  15674  trilpolemeq1  15684  trilpo  15687  apdiff  15692  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  redcwlpo  15699  redc0  15701  reap0  15702  dceqnconst  15704  dcapnconst  15705  nconstwlpolem  15709  nconstwlpo  15710  neapmkv  15712  ltlenmkv  15714