Theorem ralrimiva 2623

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

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  ralrimivvva  2633  rgen2  2636  rgen3  2637  nrexdv  2643  r19.29vva  2696  rabbidva  2809  ssrabdv  3327  ss2rabdv  3329  iuneq2dv  4031  iunssd  4056  disjeq2dv  4109  mpteq12dva  4210  triun  4240  issod  4462  frirrg  4493  frind  4495  peano2  4740  dmmptd  5512  fun11iun  5658  fniinfv  5758  eqfnfv  5800  eqfnfvd  5803  fnmptfvd  5807  dff3im  5847  dffo4  5850  fmptd  5856  ffnfv  5860  fmpt2d  5864  ffvresb  5865  funiun  5884  fconst2g  5924  fconstfvm  5927  resfunexg  5930  eufnfv  5942  foco2  5952  fniunfv  5961  fcofo  5983  fliftel  5992  fliftfun  5995  fliftfuns  5997  riota5f  6058  f1ocnvd  6285  f1o3d  6291  suppssov1  6292  offval2  6311  ofrfval2  6312  offveqb  6315  offveq  6316  caofref  6320  caofinvl  6321  caofid0l  6322  caofid0r  6323  caofid1  6324  caofid2  6325  opabex3d  6343  uchoice  6364  oprssdmm  6398  f1od2  6464  disjxp1  6465  funsssuppss  6491  suppofss1dcl  6497  suppofss2dcl  6498  tfrlem1  6572  tfrlemisucaccv  6589  tfrlemiubacc  6594  tfr1onlemsucfn  6604  tfr1onlemsucaccv  6605  tfr1onlembxssdm  6607  tfr1onlembfn  6608  tfr1onlemubacc  6610  tfr1onlemaccex  6612  tfr1onlemres  6613  tfrcllemsucfn  6617  tfrcllemsucaccv  6618  tfrcllembxssdm  6620  tfrcllembfn  6621  tfrcllemubacc  6623  tfrcllemaccex  6625  tfrcllemres  6626  tfrcl  6628  rdgon  6650  freccllem  6666  frecfcllem  6668  omcl  6727  oeicl  6728  qliftfuns  6886  ixpeq2dva  6988  xpf1o  7137  mapxpen  7141  isinfinf  7194  fimax2gtrilemstep  7198  undifdcss  7223  opabfi  7240  fissfi  7256  fdcf1  7309  f1setfi  7310  2omap  7311  eqsuptid  7330  eqinftid  7354  difinfsnlem  7432  difinfsn  7433  ctmlemr  7441  ctm  7442  ctssdclemn0  7443  ctssdccl  7444  enumctlemm  7447  nninfninc  7456  nnnninf  7459  nnnninfeq  7461  enomnilem  7471  ismkvnex  7488  enmkvlem  7494  enwomnilem  7502  nninfwlporlemd  7505  nninfwlpoimlemg  7508  nninfwlpoimlemginf  7509  nninfwlpoim  7512  nninfinfwlpo  7513  finacn  7553  acfun  7556  exmidaclem  7557  exmidontriimlem4  7573  exmidontriim  7574  pw1on  7578  ccfunen  7623  cc2lem  7625  cc3  7627  acnccim  7631  genprndl  7881  genprndu  7882  nqprloc  7905  ltexprlemrnd  7965  ltexprlemdisj  7966  lteupri  7977  recexprlemrnd  7989  recexprlemdisj  7990  caucvgprlemlim  8041  caucvgprprlemlim  8071  suplocexprlemml  8076  suplocexprlemrl  8077  suplocexprlemmu  8078  suplocexprlemru  8079  suplocexprlemdisj  8080  suplocexprlemloc  8081  suplocexprlemub  8083  caucvgsrlembound  8154  caucvgsrlemgt1  8155  caucvgsrlemoffgt1  8159  caucvgsr  8162  suplocsrlemb  8166  suplocsrlempr  8167  suplocsrlem  8168  elrealeu  8189  axcaucvglemcau  8258  axcaucvglemres  8259  axpre-suploclemres  8261  negeu  8510  eqord1  8804  eqord2  8805  creur  9282  creui  9283  suprzclex  9726  supinfneg  9977  infsupneg  9978  infregelbex  9980  indstr2  9991  iooidg  10293  iccsupr  10350  icoshftf1o  10375  fznlem  10427  exfzdc  10640  zsupcllemstep  10643  infssuzex  10647  suprzubdc  10652  zsupssdc  10654  exbtwnzlemstep  10663  exbtwnzlemex  10665  frec2uzrdg  10827  frecuzrdgrcl  10828  frecuzrdgtcl  10830  frecuzrdgsuc  10832  frecuzrdgrclt  10833  frecuzrdgg  10834  frecuzrdgfunlem  10837  frecuzrdgsuctlem  10841  nninfinf  10861  iseqovex  10876  seq3val  10878  seqvalcd  10879  seq3-1  10880  seqf  10882  seq3p1  10883  seqovcd  10885  seqp1cd  10888  seq3clss  10889  seq3fveq2  10893  seqfveq2g  10895  seqfveqg  10896  seq3fveq  10897  seq3feq  10898  seq3shft2  10899  seqshft2g  10900  monoord  10903  monoord2  10904  ser3mono  10905  seq3split  10906  seqsplitg  10907  seq3caopr3  10909  seqcaopr3g  10910  seq3caopr2  10911  seqcaopr2g  10912  iseqf1olemqk  10925  iseqf1olemjpcl  10926  iseqf1olemqpcl  10927  iseqf1olemfvp  10928  seq3f1olemqsumkj  10929  seq3f1olemqsumk  10930  seq3f1olemqsum  10931  seq3f1oleml  10934  seq3f1o  10935  seqf1og  10939  seq3id3  10942  seq3id  10943  seq3id2  10944  seq3homo  10945  seq3z  10946  seqhomog  10948  seqfeq4g  10949  ser3ge0  10954  nn0ltexp2  11128  bccl  11186  hashinfuni  11197  hashennnuni  11199  sshashneg  11262  hashfibclem  11263  hashf1lem1  11266  wrdexg  11296  ccatlen  11344  ccatvalfn  11350  ccatrn  11358  swrdlen  11405  swrdwrdsymbg  11417  swrdswrd  11458  wrdind  11475  reuccatpfxs1  11500  shftf  11576  seq3shft  11584  caucvgrelemcau  11727  cvg1nlemcau  11731  cvg1nlemres  11732  resqrexlemcvg  11766  resqrexlemglsq  11769  resqrexlemga  11770  maxabslemval  11955  negfi  11975  minmax  11977  xrmaxiflemval  11997  xrminmax  12012  climconst  12037  2clim  12048  climcn1  12055  climcn2  12056  reccn2ap  12060  cn1lem  12061  climsqz  12082  climsqz2  12083  climcau  12094  climrecvg1n  12095  serf0  12099  sumeq2dv  12115  sumrbdclem  12125  fsum3cvg  12126  summodclem3  12128  summodclem2a  12129  zsumdc  12132  isum  12133  fsumgcl  12134  fsum3  12135  fsumf1o  12138  isumss  12139  fisumss  12140  isumss2  12141  fsum3cvg2  12142  fsumsersdc  12143  fsum3ser  12145  fsumcl2lem  12146  fsumadd  12154  fsumsplit  12155  fsumm1  12164  fsum1p  12166  isumclim3  12171  isummulc2  12174  sumsplitdc  12180  fsum2dlemstep  12182  fisumcom2  12186  fsumshftm  12193  fsummulc2  12196  fsumge1  12209  fsum00  12210  fsumabs  12213  telfsumo  12214  telfsumo2  12215  fsumparts  12218  fsumrelem  12219  fsumiun  12225  hashiun  12226  hash2iun  12227  binomlem  12231  isumshft  12238  isum1p  12240  isumnn0nn  12241  isumrpcl  12242  isumlessdc  12244  divcnv  12245  cvgratnnlemnexp  12272  cvgratnnlemmn  12273  cvgratnnlemseq  12274  cvgratnnlemabsle  12275  cvgratnnlemfm  12277  cvgratnnlemrate  12278  cvgratnn  12279  cvgratz  12280  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  clim2prod  12287  prodeq2dv  12314  prodrbdclem  12319  fproddccvg  12320  prodmodclem3  12323  prodmodclem2a  12324  zproddc  12327  iprodap  12328  fprodseq  12331  fprodf1o  12336  prodssdc  12337  fprodssdc  12338  fprodmul  12339  fprodsplit  12345  fprodm1  12346  fprod1p  12347  fprodm1s  12349  fprodp1s  12350  fprodunsn  12352  fprodcl2lem  12353  fprodabs  12364  fprodeq0  12365  fprodap0  12369  fprod2dlemstep  12370  fprodcom2fi  12374  fprodrec  12377  fprodmodd  12389  efcvgfsum  12415  dvdsssfz1  12600  bitsfi  12705  bitsinv1  12710  dvdsbnd  12714  bezoutlemstep  12755  bezoutlemmain  12756  bezoutlemle  12766  bezoutlemsup  12767  dfgcd3  12768  dfgcd2  12772  nnwodc  12794  uzwodc  12795  nnwosdc  12797  nninfctlemfo  12798  coprmgcdb  12847  prmdc  12889  isprm5  12901  isprm6  12906  phivalfi  12971  phibndlem  12975  dfphi2  12979  hashdvds  12980  phiprmpw  12981  phimullem  12984  eulerthlemfi  12987  dvdsfi  12998  hashgcdeq  12999  phisum  13000  reumodprminv  13013  pclemdc  13048  pc2dvds  13090  pcz  13092  pcprmpw2  13093  pcmptdvds  13105  pcprod  13106  pcfac  13110  qexpz  13112  prmpwdvds  13115  pockthg  13117  infpnlem2  13120  1arithlem4  13126  1arith  13127  4sqlemafi  13155  4sqlemffi  13156  4sqleminfi  13157  ballotfilemcinfi  13205  ballotfilemdifcfi  13206  ballotfilemcinfz  13207  ballotfilemdifcfz  13208  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemefi  13218  ballotfilemodife  13221  ballotfilemiex  13225  ennnfonelemex  13286  ennnfonelemfun  13289  ennnfonelemf1  13290  ennnfonelemnn0  13294  ennnfonelemim  13296  exmidunben  13298  ctinfomlemom  13299  ctinfom  13300  ctinf  13302  ctiunctlemudc  13309  ctiunctlemf  13310  ctiunctlemfo  13311  omctfn  13315  ssnnctlemct  13318  nninfdclemcl  13320  nninfdclemp1  13322  imasival  13607  ismgmid2  13680  mgmidsssn0  13684  grpinvalem  13685  grpinva  13686  gzsumress  13692  issgrpd  13707  sgrpidmndm  13713  ismndd  13730  mndpfo  13731  mhmima  13778  mhmeql  13779  gsumvallem2  13780  isgrpd2e  13805  dfgrp2  13812  grpidd2  13826  isgrpinv  13839  grplrinv  13842  grpidinv  13844  dfgrp3me  13885  mhmmnd  13899  ghmgrp  13901  mulgsubcl  13919  issubg2m  13972  issubgrpd2  13973  grpissubg  13977  subgintm  13981  nmzsubg  13993  ssnmz  13994  ghmrn  14040  ghmeql  14050  ghmf1  14056  conjnmz  14062  conjnmzb  14063  rinvmod  14093  gsummptfidmadd  14141  prdsplusgsgrpcl  14170  prdsplusgcl  14172  prdsidlem  14173  prdsinvlem  14176  pwsbas  14185  srgrz  14265  srglz  14266  srgisid  14267  ringsrg  14328  rhmdvdsr  14458  rhmopp  14459  subrngintm  14496  subrg1  14515  subrgugrp  14524  subrgintm  14527  rrgsupp  14550  unitrrg  14552  aprap  14574  islmodd  14605  lssuni  14675  lsssubg  14689  lssintclm  14696  dflidl2rng  14793  lidlsubg  14798  cnsubglem  14891  gsumfsum  14898  znf1o  14961  znidomb  14968  psrbagfi  14985  psrbaglecl  14986  psrbagcon  14988  psr1clfi  15005  mplsubgfilemm  15015  mplsubgfilemcl  15016  mplsubgfi  15018  fiinbas  15076  tgclb  15092  restbasg  15195  iscnp4  15245  cnco  15248  cnptopco  15249  cnss1  15253  cnss2  15254  cncnpi  15255  cncnp  15257  cnconst2  15260  cnrest  15262  cnptopresti  15265  cnpdis  15269  lmtopcnp  15277  txbasval  15294  tx1cn  15296  tx2cn  15297  txcnp  15298  upxp  15299  txdis1cn  15305  cnmpt11  15310  psmet0  15354  psmettri2  15355  psmetxrge0  15359  psmetres2  15360  ismeti  15373  xmetpsmet  15396  blsscls2  15520  comet  15526  xmettx  15537  tgioo  15581  tgqioo  15582  fsumcncntop  15594  elcncf1di  15606  cdivcncfap  15631  mulcncflem  15634  mulcncf  15635  cnopnap  15638  divcncfap  15641  dedekindeulemuub  15644  dedekindeulemlu  15648  suplociccreex  15651  suplociccex  15652  dedekindicclemuub  15653  dedekindicclemlu  15657  ivthinclemlopn  15663  ivthinclemlr  15664  ivthinclemuopn  15665  ivthinclemur  15666  ivthinclemdisj  15667  ivthinclemloc  15668  ivthinc  15670  ivthdec  15671  dich0  15679  ivthdich  15680  cnplimclemr  15696  limccnp2cntop  15704  limccoap  15705  dvcn  15727  dvfre  15737  dvrecap  15740  dvmptclx  15745  dvmptaddx  15746  dvmptmulx  15747  dveflem  15753  dvef  15754  ply1termlem  15769  plyaddlem1  15774  plymullem1  15775  plycoeid3  15784  plycj  15788  plyreres  15791  dvply1  15792  sin0pilem1  15808  sin0pilem2  15809  mpodvdsmulf1o  16021  mersenne  16028  perfectlem2  16031  lgsval2lem  16046  lgsdirnn0  16083  lgsdinn0  16084  gausslemma2dlem1f1o  16096  gausslemma2dlem2  16098  gausslemma2dlem3  16099  lgsquadlemofi  16112  lgsquadlem1  16113  lgsquadlem2  16114  2lgslem1a1  16122  2sqlem6  16156  2sqlem8  16159  2sqlem10  16161  usgruspgrben  16344  uspgredg2v  16379  usgredg2v  16382  subuhgr  16430  subupgr  16431  subumgr  16432  subusgr  16433  vtxedgfi  16447  vtxlpfi  16448  wlk1walkdom  16517  wlkres  16537  eupth2lembfi  16635  depindlem1  16664  depindlem2  16665  depindlem3  16666  dichmul0or  16677  fnmptd  16749  bj-charfun  16750  bj-charfundc  16751  bj-charfunr  16753  pw1nct  16950  nnsf  16956  nninfalllem1  16959  nninfall  16960  nninfself  16964  nninfsellemeq  16965  nninfsellemeqinf  16967  nninfsel  16968  nnnninfex  16973  nninfnfiinf  16974  repiecef  16985  isomninnlem  16987  trilpolemeq1  16997  trilpo  17000  apdiff  17005  iswomninnlem  17007  iswomni0  17009  ismkvnnlem  17010  redcwlpo  17013  redc0  17015  reap0  17016  dceqnconst  17018  dcapnconst  17019  nconstwlpolem  17023  nconstwlpo  17024  neapmkv  17026  ltlenmkv  17028