Theorem ralrimiva 2550

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralrimivvva  2560  rgen2  2563  rgen3  2564  nrexdv  2570  r19.29vva  2622  rabbidva  2725  ssrabdv  3234  ss2rabdv  3236  iuneq2dv  3907  iunssd  3932  disjeq2dv  3985  mpteq12dva  4084  triun  4114  issod  4319  frirrg  4350  frind  4352  peano2  4594  dmmptd  5346  fun11iun  5482  fniinfv  5574  eqfnfv  5613  eqfnfvd  5616  fnmptfvd  5620  dff3im  5661  dffo4  5664  fmptd  5670  ffnfv  5674  fmpt2d  5678  ffvresb  5679  fconst2g  5731  fconstfvm  5734  resfunexg  5737  eufnfv  5747  foco2  5754  fniunfv  5762  fcofo  5784  fliftel  5793  fliftfun  5796  fliftfuns  5798  riota5f  5854  f1ocnvd  6072  suppssov1  6079  offval2  6097  ofrfval2  6098  offveqb  6101  caofref  6103  caofinvl  6104  opabex3d  6121  oprssdmm  6171  f1od2  6235  disjxp1  6236  tfrlem1  6308  tfrlemisucaccv  6325  tfrlemiubacc  6330  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemubacc  6346  tfr1onlemaccex  6348  tfr1onlemres  6349  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemubacc  6359  tfrcllemaccex  6361  tfrcllemres  6362  tfrcl  6364  rdgon  6386  freccllem  6402  frecfcllem  6404  omcl  6461  oeicl  6462  qliftfuns  6618  ixpeq2dva  6712  xpf1o  6843  mapxpen  6847  isinfinf  6896  fimax2gtrilemstep  6899  undifdcss  6921  eqsuptid  6995  eqinftid  7019  difinfsnlem  7097  difinfsn  7098  ctmlemr  7106  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  enumctlemm  7112  nnnninf  7123  nnnninfeq  7125  enomnilem  7135  ismkvnex  7152  enmkvlem  7158  enwomnilem  7166  nninfwlporlemd  7169  nninfwlpoimlemg  7172  nninfwlpoimlemginf  7173  nninfwlpoim  7175  acfun  7205  exmidaclem  7206  exmidontriimlem4  7222  exmidontriim  7223  pw1on  7224  ccfunen  7262  cc2lem  7264  cc3  7266  genprndl  7519  genprndu  7520  nqprloc  7543  ltexprlemrnd  7603  ltexprlemdisj  7604  lteupri  7615  recexprlemrnd  7627  recexprlemdisj  7628  caucvgprlemlim  7679  caucvgprprlemlim  7709  suplocexprlemml  7714  suplocexprlemrl  7715  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  caucvgsrlembound  7792  caucvgsrlemgt1  7793  caucvgsrlemoffgt1  7797  caucvgsr  7800  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  elrealeu  7827  axcaucvglemcau  7896  axcaucvglemres  7897  axpre-suploclemres  7899  negeu  8147  eqord1  8439  eqord2  8440  creur  8915  creui  8916  suprzclex  9350  supinfneg  9594  infsupneg  9595  infregelbex  9597  indstr2  9608  iooidg  9908  iccsupr  9965  icoshftf1o  9990  fznlem  10040  exfzdc  10239  exbtwnzlemstep  10247  exbtwnzlemex  10249  frec2uzrdg  10408  frecuzrdgrcl  10409  frecuzrdgtcl  10411  frecuzrdgsuc  10413  frecuzrdgrclt  10414  frecuzrdgg  10415  frecuzrdgfunlem  10418  frecuzrdgsuctlem  10422  iseqovex  10455  seq3val  10457  seqvalcd  10458  seq3-1  10459  seqf  10460  seq3p1  10461  seqovcd  10462  seqp1cd  10465  seq3clss  10466  seq3fveq2  10468  seq3fveq  10470  seq3feq  10471  seq3shft2  10472  monoord  10475  monoord2  10476  ser3mono  10477  seq3split  10478  seq3caopr3  10480  seq3caopr2  10481  iseqf1olemqk  10493  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  iseqf1olemfvp  10496  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1oleml  10502  seq3f1o  10503  seq3id3  10506  seq3id  10507  seq3id2  10508  seq3homo  10509  seq3z  10510  ser3ge0  10516  nn0ltexp2  10688  bccl  10746  hashinfuni  10756  hashennnuni  10758  shftf  10838  seq3shft  10846  caucvgrelemcau  10988  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemcvg  11027  resqrexlemglsq  11030  resqrexlemga  11031  maxabslemval  11216  negfi  11235  minmax  11237  xrmaxiflemval  11257  xrminmax  11272  climconst  11297  2clim  11308  climcn1  11315  climcn2  11316  reccn2ap  11320  cn1lem  11321  climsqz  11342  climsqz2  11343  climcau  11354  climrecvg1n  11355  serf0  11359  sumeq2dv  11375  sumrbdclem  11384  fsum3cvg  11385  summodclem3  11387  summodclem2a  11388  zsumdc  11391  isum  11392  fsumgcl  11393  fsum3  11394  fsumf1o  11397  isumss  11398  fisumss  11399  isumss2  11400  fsum3cvg2  11401  fsumsersdc  11402  fsum3ser  11404  fsumcl2lem  11405  fsumadd  11413  fsumsplit  11414  fsumm1  11423  fsum1p  11425  isumclim3  11430  isummulc2  11433  sumsplitdc  11439  fsum2dlemstep  11441  fisumcom2  11445  fsumshftm  11452  fsummulc2  11455  fsumge1  11468  fsum00  11469  fsumabs  11472  telfsumo  11473  telfsumo2  11474  fsumparts  11477  fsumrelem  11478  fsumiun  11484  hashiun  11485  hash2iun  11486  binomlem  11490  isumshft  11497  isum1p  11499  isumnn0nn  11500  isumrpcl  11501  isumlessdc  11503  divcnv  11504  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemseq  11533  cvgratnnlemabsle  11534  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratnn  11538  cvgratz  11539  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  clim2prod  11546  prodeq2dv  11573  prodrbdclem  11578  fproddccvg  11579  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  iprodap  11587  fprodseq  11590  fprodf1o  11595  prodssdc  11596  fprodssdc  11597  fprodmul  11598  fprodsplit  11604  fprodm1  11605  fprod1p  11606  fprodm1s  11608  fprodp1s  11609  fprodunsn  11611  fprodcl2lem  11612  fprodabs  11623  fprodeq0  11624  fprodap0  11628  fprod2dlemstep  11629  fprodcom2fi  11633  fprodrec  11636  fprodmodd  11648  efcvgfsum  11674  dvdsssfz1  11857  zsupcllemstep  11945  infssuzex  11949  suprzubdc  11952  zsupssdc  11954  dvdsbnd  11956  bezoutlemstep  11997  bezoutlemmain  11998  bezoutlemle  12008  bezoutlemsup  12009  dfgcd3  12010  dfgcd2  12014  nnwodc  12036  uzwodc  12037  nnwosdc  12039  coprmgcdb  12087  prmdc  12129  isprm5  12141  isprm6  12146  phivalfi  12211  phibndlem  12215  dfphi2  12219  hashdvds  12220  phiprmpw  12221  phimullem  12224  eulerthlemfi  12227  hashgcdeq  12238  phisum  12239  reumodprminv  12252  pclemdc  12287  pc2dvds  12328  pcz  12330  pcprmpw2  12331  pcmptdvds  12342  pcprod  12343  pcfac  12347  qexpz  12349  prmpwdvds  12352  pockthg  12354  infpnlem2  12357  1arithlem4  12363  1arith  12364  ennnfonelemex  12414  ennnfonelemfun  12417  ennnfonelemf1  12418  ennnfonelemnn0  12422  ennnfonelemim  12424  exmidunben  12426  ctinfomlemom  12427  ctinfom  12428  ctinf  12430  ctiunctlemudc  12437  ctiunctlemf  12438  ctiunctlemfo  12439  omctfn  12443  ssnnctlemct  12446  nninfdclemcl  12448  nninfdclemp1  12450  imasival  12726  ismgmid2  12798  mgmidsssn0  12802  grprinvlem  12803  grprinvd  12804  sgrpidmndm  12820  ismndd  12837  mndpfo  12838  mhmima  12874  mhmeql  12875  isgrpd2e  12895  dfgrp2  12901  grpidd2  12913  isgrpinv  12925  grplrinv  12926  grpidinv  12928  dfgrp3me  12969  mhmmnd  12979  ghmgrp  12981  mulgsubcl  12996  issubg2m  13047  issubgrpd2  13048  grpissubg  13052  subgintm  13056  nmzsubg  13068  ssnmz  13069  rinvmod  13110  srgrz  13165  srglz  13166  srgisid  13167  ringsrg  13222  subrg1  13350  subrgugrp  13359  subrgintm  13362  aprap  13374  islmodd  13381  cnsubglem  13443  fiinbas  13519  tgclb  13535  restbasg  13638  iscnp4  13688  cnco  13691  cnptopco  13692  cnss1  13696  cnss2  13697  cncnpi  13698  cncnp  13700  cnconst2  13703  cnrest  13705  cnptopresti  13708  cnpdis  13712  lmtopcnp  13720  txbasval  13737  tx1cn  13739  tx2cn  13740  txcnp  13741  upxp  13742  txdis1cn  13748  cnmpt11  13753  psmet0  13797  psmettri2  13798  psmetxrge0  13802  psmetres2  13803  ismeti  13816  xmetpsmet  13839  blsscls2  13963  comet  13969  xmettx  13980  tgioo  14016  tgqioo  14017  fsumcncntop  14026  elcncf1di  14036  cdivcncfap  14057  mulcncflem  14060  mulcncf  14061  cnopnap  14064  dedekindeulemuub  14065  dedekindeulemlu  14069  suplociccreex  14072  suplociccex  14073  dedekindicclemuub  14074  dedekindicclemlu  14078  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemdisj  14088  ivthinclemloc  14089  ivthinc  14091  ivthdec  14092  cnplimclemr  14108  limccnp2cntop  14116  limccoap  14117  dvcn  14134  dvfre  14144  dvrecap  14147  dvmptclx  14150  dvmptaddx  14151  dvmptmulx  14152  dveflem  14157  dvef  14158  sin0pilem1  14172  sin0pilem2  14173  lgsval2lem  14381  lgsdirnn0  14418  lgsdinn0  14419  2sqlem6  14437  2sqlem8  14440  2sqlem10  14442  fnmptd  14526  bj-charfun  14529  bj-charfundc  14530  bj-charfunr  14532  pw1nct  14722  nnsf  14724  nninfalllem1  14727  nninfall  14728  nninfself  14732  nninfsellemeq  14733  nninfsellemeqinf  14735  nninfsel  14736  isomninnlem  14748  trilpolemeq1  14758  trilpo  14761  apdiff  14766  iswomninnlem  14767  iswomni0  14769  ismkvnnlem  14770  redcwlpo  14773  redc0  14775  reap0  14776  dceqnconst  14777  dcapnconst  14778  nconstwlpolem  14782  nconstwlpo  14783  neapmkv  14785  ltlenmkv  14787