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  10487  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  zsupssdc  10499  exbtwnzlemstep  10508  exbtwnzlemex  10510  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  nninfinf  10706  iseqovex  10721  seq3val  10723  seqvalcd  10724  seq3-1  10725  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seqfveqg  10741  seq3fveq  10742  seq3feq  10743  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1og  10784  seq3id3  10787  seq3id  10788  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  nn0ltexp2  10972  bccl  11030  hashinfuni  11040  hashennnuni  11042  wrdexg  11125  ccatlen  11173  ccatvalfn  11179  ccatrn  11187  swrdlen  11234  swrdwrdsymbg  11246  swrdswrd  11287  wrdind  11304  reuccatpfxs1  11329  shftf  11392  seq3shft  11400  caucvgrelemcau  11542  cvg1nlemcau  11546  cvg1nlemres  11547  resqrexlemcvg  11581  resqrexlemglsq  11584  resqrexlemga  11585  maxabslemval  11770  negfi  11790  minmax  11792  xrmaxiflemval  11812  xrminmax  11827  climconst  11852  2clim  11863  climcn1  11870  climcn2  11871  reccn2ap  11875  cn1lem  11876  climsqz  11897  climsqz2  11898  climcau  11909  climrecvg1n  11910  serf0  11914  sumeq2dv  11930  sumrbdclem  11940  fsum3cvg  11941  summodclem3  11943  summodclem2a  11944  zsumdc  11947  isum  11948  fsumgcl  11949  fsum3  11950  fsumf1o  11953  isumss  11954  fisumss  11955  isumss2  11956  fsum3cvg2  11957  fsumsersdc  11958  fsum3ser  11960  fsumcl2lem  11961  fsumadd  11969  fsumsplit  11970  fsumm1  11979  fsum1p  11981  isumclim3  11986  isummulc2  11989  sumsplitdc  11995  fsum2dlemstep  11997  fisumcom2  12001  fsumshftm  12008  fsummulc2  12011  fsumge1  12024  fsum00  12025  fsumabs  12028  telfsumo  12029  telfsumo2  12030  fsumparts  12033  fsumrelem  12034  fsumiun  12040  hashiun  12041  hash2iun  12042  binomlem  12046  isumshft  12053  isum1p  12055  isumnn0nn  12056  isumrpcl  12057  isumlessdc  12059  divcnv  12060  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  cvgratnnlemseq  12089  cvgratnnlemabsle  12090  cvgratnnlemfm  12092  cvgratnnlemrate  12093  cvgratnn  12094  cvgratz  12095  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  clim2prod  12102  prodeq2dv  12129  prodrbdclem  12134  fproddccvg  12135  prodmodclem3  12138  prodmodclem2a  12139  zproddc  12142  iprodap  12143  fprodseq  12146  fprodf1o  12151  prodssdc  12152  fprodssdc  12153  fprodmul  12154  fprodsplit  12160  fprodm1  12161  fprod1p  12162  fprodm1s  12164  fprodp1s  12165  fprodunsn  12167  fprodcl2lem  12168  fprodabs  12179  fprodeq0  12180  fprodap0  12184  fprod2dlemstep  12185  fprodcom2fi  12189  fprodrec  12192  fprodmodd  12204  efcvgfsum  12230  dvdsssfz1  12415  bitsfi  12520  bitsinv1  12525  dvdsbnd  12529  bezoutlemstep  12570  bezoutlemmain  12571  bezoutlemle  12581  bezoutlemsup  12582  dfgcd3  12583  dfgcd2  12587  nnwodc  12609  uzwodc  12610  nnwosdc  12612  nninfctlemfo  12613  coprmgcdb  12662  prmdc  12704  isprm5  12716  isprm6  12721  phivalfi  12786  phibndlem  12790  dfphi2  12794  hashdvds  12795  phiprmpw  12796  phimullem  12799  eulerthlemfi  12802  dvdsfi  12813  hashgcdeq  12814  phisum  12815  reumodprminv  12828  pclemdc  12863  pc2dvds  12905  pcz  12907  pcprmpw2  12908  pcmptdvds  12920  pcprod  12921  pcfac  12925  qexpz  12927  prmpwdvds  12930  pockthg  12932  infpnlem2  12935  1arithlem4  12941  1arith  12942  4sqlemafi  12970  4sqlemffi  12971  4sqleminfi  12972  ennnfonelemex  13037  ennnfonelemfun  13040  ennnfonelemf1  13041  ennnfonelemnn0  13045  ennnfonelemim  13047  exmidunben  13049  ctinfomlemom  13050  ctinfom  13051  ctinf  13053  ctiunctlemudc  13060  ctiunctlemf  13061  ctiunctlemfo  13062  omctfn  13066  ssnnctlemct  13069  nninfdclemcl  13071  nninfdclemp1  13073  pwsbas  13377  imasival  13391  ismgmid2  13465  mgmidsssn0  13469  grpinvalem  13470  grpinva  13471  gsumress  13480  issgrpd  13497  prdsplusgsgrpcl  13499  sgrpidmndm  13505  ismndd  13522  mndpfo  13523  prdsplusgcl  13531  prdsidlem  13532  mhmima  13576  mhmeql  13577  gsumvallem2  13578  isgrpd2e  13605  dfgrp2  13612  grpidd2  13626  isgrpinv  13639  grplrinv  13642  grpidinv  13644  dfgrp3me  13685  prdsinvlem  13693  mhmmnd  13705  ghmgrp  13707  mulgsubcl  13725  issubg2m  13778  issubgrpd2  13779  grpissubg  13783  subgintm  13787  nmzsubg  13799  ssnmz  13800  ghmrn  13846  ghmeql  13856  ghmf1  13862  conjnmz  13868  conjnmzb  13869  rinvmod  13898  srgrz  14000  srglz  14001  srgisid  14002  ringsrg  14063  rhmdvdsr  14192  rhmopp  14193  subrngintm  14229  subrg1  14248  subrgugrp  14257  subrgintm  14260  unitrrg  14284  aprap  14303  islmodd  14310  lssuni  14380  lsssubg  14394  lssintclm  14401  dflidl2rng  14498  lidlsubg  14503  cnsubglem  14596  gsumfzfsumlemm  14604  znf1o  14668  znidomb  14675  psrbagfi  14690  psr1clfi  14705  mplsubgfilemm  14715  mplsubgfilemcl  14716  mplsubgfi  14718  fiinbas  14776  tgclb  14792  restbasg  14895  iscnp4  14945  cnco  14948  cnptopco  14949  cnss1  14953  cnss2  14954  cncnpi  14955  cncnp  14957  cnconst2  14960  cnrest  14962  cnptopresti  14965  cnpdis  14969  lmtopcnp  14977  txbasval  14994  tx1cn  14996  tx2cn  14997  txcnp  14998  upxp  14999  txdis1cn  15005  cnmpt11  15010  psmet0  15054  psmettri2  15055  psmetxrge0  15059  psmetres2  15060  ismeti  15073  xmetpsmet  15096  blsscls2  15220  comet  15226  xmettx  15237  tgioo  15281  tgqioo  15282  fsumcncntop  15294  elcncf1di  15306  cdivcncfap  15331  mulcncflem  15334  mulcncf  15335  cnopnap  15338  divcncfap  15341  dedekindeulemuub  15344  dedekindeulemlu  15348  suplociccreex  15351  suplociccex  15352  dedekindicclemuub  15353  dedekindicclemlu  15357  ivthinclemlopn  15363  ivthinclemlr  15364  ivthinclemuopn  15365  ivthinclemur  15366  ivthinclemdisj  15367  ivthinclemloc  15368  ivthinc  15370  ivthdec  15371  dich0  15379  ivthdich  15380  cnplimclemr  15396  limccnp2cntop  15404  limccoap  15405  dvcn  15427  dvfre  15437  dvrecap  15440  dvmptclx  15445  dvmptaddx  15446  dvmptmulx  15447  dveflem  15453  dvef  15454  ply1termlem  15469  plyaddlem1  15474  plymullem1  15475  plycoeid3  15484  plycj  15488  plyreres  15491  dvply1  15492  sin0pilem1  15508  sin0pilem2  15509  mpodvdsmulf1o  15717  mersenne  15724  perfectlem2  15727  lgsval2lem  15742  lgsdirnn0  15779  lgsdinn0  15780  gausslemma2dlem1f1o  15792  gausslemma2dlem2  15794  gausslemma2dlem3  15795  lgsquadlemofi  15808  lgsquadlem1  15809  lgsquadlem2  15810  2lgslem1a1  15818  2sqlem6  15852  2sqlem8  15855  2sqlem10  15857  usgruspgrben  16040  uspgredg2v  16075  usgredg2v  16078  subuhgr  16126  subupgr  16127  subumgr  16128  subusgr  16129  vtxedgfi  16143  vtxlpfi  16144  wlk1walkdom  16213  wlkres  16233  eupth2lembfi  16331  depindlem1  16346  depindlem2  16347  depindlem3  16348  fnmptd  16421  bj-charfun  16423  bj-charfundc  16424  bj-charfunr  16426  2omap  16615  pw1nct  16625  nnsf  16628  nninfalllem1  16631  nninfall  16632  nninfself  16636  nninfsellemeq  16637  nninfsellemeqinf  16639  nninfsel  16640  nnnninfex  16645  nninfnfiinf  16646  isomninnlem  16655  trilpolemeq1  16665  trilpo  16668  apdiff  16673  iswomninnlem  16674  iswomni0  16676  ismkvnnlem  16677  redcwlpo  16680  redc0  16682  reap0  16683  dceqnconst  16685  dcapnconst  16686  nconstwlpolem  16690  nconstwlpo  16691  neapmkv  16693  ltlenmkv  16695