Theorem ralrimiva 2567

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralrimivvva  2577  rgen2  2580  rgen3  2581  nrexdv  2587  r19.29vva  2639  rabbidva  2748  ssrabdv  3258  ss2rabdv  3260  iuneq2dv  3933  iunssd  3958  disjeq2dv  4011  mpteq12dva  4110  triun  4140  issod  4350  frirrg  4381  frind  4383  peano2  4627  dmmptd  5384  fun11iun  5521  fniinfv  5615  eqfnfv  5655  eqfnfvd  5658  fnmptfvd  5662  dff3im  5703  dffo4  5706  fmptd  5712  ffnfv  5716  fmpt2d  5720  ffvresb  5721  fconst2g  5773  fconstfvm  5776  resfunexg  5779  eufnfv  5789  foco2  5796  fniunfv  5805  fcofo  5827  fliftel  5836  fliftfun  5839  fliftfuns  5841  riota5f  5898  f1ocnvd  6120  suppssov1  6127  offval2  6146  ofrfval2  6147  offveqb  6150  caofref  6154  caofinvl  6155  opabex3d  6173  uchoice  6190  oprssdmm  6224  f1od2  6288  disjxp1  6289  tfrlem1  6361  tfrlemisucaccv  6378  tfrlemiubacc  6383  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemubacc  6399  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemubacc  6412  tfrcllemaccex  6414  tfrcllemres  6415  tfrcl  6417  rdgon  6439  freccllem  6455  frecfcllem  6457  omcl  6514  oeicl  6515  qliftfuns  6673  ixpeq2dva  6767  xpf1o  6900  mapxpen  6904  isinfinf  6953  fimax2gtrilemstep  6956  undifdcss  6979  opabfi  6992  eqsuptid  7056  eqinftid  7080  difinfsnlem  7158  difinfsn  7159  ctmlemr  7167  ctm  7168  ctssdclemn0  7169  ctssdccl  7170  enumctlemm  7173  nninfninc  7182  nnnninf  7185  nnnninfeq  7187  enomnilem  7197  ismkvnex  7214  enmkvlem  7220  enwomnilem  7228  nninfwlporlemd  7231  nninfwlpoimlemg  7234  nninfwlpoimlemginf  7235  nninfwlpoim  7237  acfun  7267  exmidaclem  7268  exmidontriimlem4  7284  exmidontriim  7285  pw1on  7286  ccfunen  7324  cc2lem  7326  cc3  7328  genprndl  7581  genprndu  7582  nqprloc  7605  ltexprlemrnd  7665  ltexprlemdisj  7666  lteupri  7677  recexprlemrnd  7689  recexprlemdisj  7690  caucvgprlemlim  7741  caucvgprprlemlim  7771  suplocexprlemml  7776  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  caucvgsrlembound  7854  caucvgsrlemgt1  7855  caucvgsrlemoffgt1  7859  caucvgsr  7862  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  elrealeu  7889  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  negeu  8210  eqord1  8502  eqord2  8503  creur  8978  creui  8979  suprzclex  9415  supinfneg  9660  infsupneg  9661  infregelbex  9663  indstr2  9674  iooidg  9975  iccsupr  10032  icoshftf1o  10057  fznlem  10107  exfzdc  10307  exbtwnzlemstep  10316  exbtwnzlemex  10318  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgtcl  10483  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgfunlem  10490  frecuzrdgsuctlem  10494  nninfinf  10514  iseqovex  10529  seq3val  10531  seqvalcd  10532  seq3-1  10533  seqf  10535  seq3p1  10536  seqovcd  10538  seqp1cd  10541  seq3clss  10542  seq3fveq2  10546  seqfveq2g  10548  seqfveqg  10549  seq3fveq  10550  seq3feq  10551  seq3shft2  10552  seqshft2g  10553  monoord  10556  monoord2  10557  ser3mono  10558  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemqk  10578  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1oleml  10587  seq3f1o  10588  seqf1og  10592  seq3id3  10595  seq3id  10596  seq3id2  10597  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  ser3ge0  10607  nn0ltexp2  10780  bccl  10838  hashinfuni  10848  hashennnuni  10850  wrdexg  10925  shftf  10974  seq3shft  10982  caucvgrelemcau  11124  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemcvg  11163  resqrexlemglsq  11166  resqrexlemga  11167  maxabslemval  11352  negfi  11371  minmax  11373  xrmaxiflemval  11393  xrminmax  11408  climconst  11433  2clim  11444  climcn1  11451  climcn2  11452  reccn2ap  11456  cn1lem  11457  climsqz  11478  climsqz2  11479  climcau  11490  climrecvg1n  11491  serf0  11495  sumeq2dv  11511  sumrbdclem  11520  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  zsumdc  11527  isum  11528  fsumgcl  11529  fsum3  11530  fsumf1o  11533  isumss  11534  fisumss  11535  isumss2  11536  fsum3cvg2  11537  fsumsersdc  11538  fsum3ser  11540  fsumcl2lem  11541  fsumadd  11549  fsumsplit  11550  fsumm1  11559  fsum1p  11561  isumclim3  11566  isummulc2  11569  sumsplitdc  11575  fsum2dlemstep  11577  fisumcom2  11581  fsumshftm  11588  fsummulc2  11591  fsumge1  11604  fsum00  11605  fsumabs  11608  telfsumo  11609  telfsumo2  11610  fsumparts  11613  fsumrelem  11614  fsumiun  11620  hashiun  11621  hash2iun  11622  binomlem  11626  isumshft  11633  isum1p  11635  isumnn0nn  11636  isumrpcl  11637  isumlessdc  11639  divcnv  11640  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemseq  11669  cvgratnnlemabsle  11670  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratnn  11674  cvgratz  11675  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  clim2prod  11682  prodeq2dv  11709  prodrbdclem  11714  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  iprodap  11723  fprodseq  11726  fprodf1o  11731  prodssdc  11732  fprodssdc  11733  fprodmul  11734  fprodsplit  11740  fprodm1  11741  fprod1p  11742  fprodm1s  11744  fprodp1s  11745  fprodunsn  11747  fprodcl2lem  11748  fprodabs  11759  fprodeq0  11760  fprodap0  11764  fprod2dlemstep  11765  fprodcom2fi  11769  fprodrec  11772  fprodmodd  11784  efcvgfsum  11810  dvdsssfz1  11994  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  zsupssdc  12091  dvdsbnd  12093  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemle  12145  bezoutlemsup  12146  dfgcd3  12147  dfgcd2  12151  nnwodc  12173  uzwodc  12174  nnwosdc  12176  nninfctlemfo  12177  coprmgcdb  12226  prmdc  12268  isprm5  12280  isprm6  12285  phivalfi  12350  phibndlem  12354  dfphi2  12358  hashdvds  12359  phiprmpw  12360  phimullem  12363  eulerthlemfi  12366  hashgcdeq  12377  phisum  12378  reumodprminv  12391  pclemdc  12426  pc2dvds  12468  pcz  12470  pcprmpw2  12471  pcmptdvds  12483  pcprod  12484  pcfac  12488  qexpz  12490  prmpwdvds  12493  pockthg  12495  infpnlem2  12498  1arithlem4  12504  1arith  12505  4sqlemafi  12533  4sqlemffi  12534  4sqleminfi  12535  ennnfonelemex  12571  ennnfonelemfun  12574  ennnfonelemf1  12575  ennnfonelemnn0  12579  ennnfonelemim  12581  exmidunben  12583  ctinfomlemom  12584  ctinfom  12585  ctinf  12587  ctiunctlemudc  12594  ctiunctlemf  12595  ctiunctlemfo  12596  omctfn  12600  ssnnctlemct  12603  nninfdclemcl  12605  nninfdclemp1  12607  imasival  12889  ismgmid2  12963  mgmidsssn0  12967  grpinvalem  12968  grpinva  12969  gsumress  12978  issgrpd  12995  sgrpidmndm  13001  ismndd  13018  mndpfo  13019  mhmima  13063  mhmeql  13064  gsumvallem2  13065  isgrpd2e  13092  dfgrp2  13099  grpidd2  13113  isgrpinv  13126  grplrinv  13129  grpidinv  13131  dfgrp3me  13172  mhmmnd  13186  ghmgrp  13188  mulgsubcl  13206  issubg2m  13259  issubgrpd2  13260  grpissubg  13264  subgintm  13268  nmzsubg  13280  ssnmz  13281  ghmrn  13327  ghmeql  13337  ghmf1  13343  conjnmz  13349  conjnmzb  13350  rinvmod  13379  srgrz  13480  srglz  13481  srgisid  13482  ringsrg  13543  rhmdvdsr  13671  rhmopp  13672  subrngintm  13708  subrg1  13727  subrgugrp  13736  subrgintm  13739  unitrrg  13763  aprap  13782  islmodd  13789  lssuni  13859  lsssubg  13873  lssintclm  13880  dflidl2rng  13977  lidlsubg  13982  cnsubglem  14067  gsumfzfsumlemm  14075  znf1o  14139  znidomb  14146  fiinbas  14217  tgclb  14233  restbasg  14336  iscnp4  14386  cnco  14389  cnptopco  14390  cnss1  14394  cnss2  14395  cncnpi  14396  cncnp  14398  cnconst2  14401  cnrest  14403  cnptopresti  14406  cnpdis  14410  lmtopcnp  14418  txbasval  14435  tx1cn  14437  tx2cn  14438  txcnp  14439  upxp  14440  txdis1cn  14446  cnmpt11  14451  psmet0  14495  psmettri2  14496  psmetxrge0  14500  psmetres2  14501  ismeti  14514  xmetpsmet  14537  blsscls2  14661  comet  14667  xmettx  14678  tgioo  14714  tgqioo  14715  fsumcncntop  14724  elcncf1di  14734  cdivcncfap  14758  mulcncflem  14761  mulcncf  14762  cnopnap  14765  divcncfap  14768  dedekindeulemuub  14771  dedekindeulemlu  14775  suplociccreex  14778  suplociccex  14779  dedekindicclemuub  14780  dedekindicclemlu  14784  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemdisj  14794  ivthinclemloc  14795  ivthinc  14797  ivthdec  14798  dich0  14806  ivthdich  14807  cnplimclemr  14823  limccnp2cntop  14831  limccoap  14832  dvcn  14849  dvfre  14859  dvrecap  14862  dvmptclx  14865  dvmptaddx  14866  dvmptmulx  14867  dveflem  14872  dvef  14873  ply1termlem  14888  plyaddlem1  14893  plymullem1  14894  sin0pilem1  14916  sin0pilem2  14917  lgsval2lem  15126  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1f1o  15176  gausslemma2dlem2  15178  gausslemma2dlem3  15179  lgsquadlem1  15191  2sqlem6  15207  2sqlem8  15210  2sqlem10  15212  fnmptd  15296  bj-charfun  15299  bj-charfundc  15300  bj-charfunr  15302  pw1nct  15493  nnsf  15495  nninfalllem1  15498  nninfall  15499  nninfself  15503  nninfsellemeq  15504  nninfsellemeqinf  15506  nninfsel  15507  isomninnlem  15520  trilpolemeq1  15530  trilpo  15533  apdiff  15538  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  redcwlpo  15545  redc0  15547  reap0  15548  dceqnconst  15550  dcapnconst  15551  nconstwlpolem  15555  nconstwlpo  15556  neapmkv  15558  ltlenmkv  15560