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  3263  ss2rabdv  3265  iuneq2dv  3938  iunssd  3963  disjeq2dv  4016  mpteq12dva  4115  triun  4145  issod  4355  frirrg  4386  frind  4388  peano2  4632  dmmptd  5391  fun11iun  5528  fniinfv  5622  eqfnfv  5662  eqfnfvd  5665  fnmptfvd  5669  dff3im  5710  dffo4  5713  fmptd  5719  ffnfv  5723  fmpt2d  5727  ffvresb  5728  fconst2g  5780  fconstfvm  5783  resfunexg  5786  eufnfv  5796  foco2  5803  fniunfv  5812  fcofo  5834  fliftel  5843  fliftfun  5846  fliftfuns  5848  riota5f  5905  f1ocnvd  6129  suppssov1  6136  offval2  6155  ofrfval2  6156  offveqb  6159  offveq  6160  caofref  6164  caofinvl  6165  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  opabex3d  6187  uchoice  6204  oprssdmm  6238  f1od2  6302  disjxp1  6303  tfrlem1  6375  tfrlemisucaccv  6392  tfrlemiubacc  6397  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemubacc  6413  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemubacc  6426  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  rdgon  6453  freccllem  6469  frecfcllem  6471  omcl  6528  oeicl  6529  qliftfuns  6687  ixpeq2dva  6781  xpf1o  6914  mapxpen  6918  isinfinf  6967  fimax2gtrilemstep  6970  undifdcss  6993  opabfi  7008  eqsuptid  7072  eqinftid  7096  difinfsnlem  7174  difinfsn  7175  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  enumctlemm  7189  nninfninc  7198  nnnninf  7201  nnnninfeq  7203  enomnilem  7213  ismkvnex  7230  enmkvlem  7236  enwomnilem  7244  nninfwlporlemd  7247  nninfwlpoimlemg  7250  nninfwlpoimlemginf  7251  nninfwlpoim  7254  nninfinfwlpo  7255  finacn  7289  acfun  7292  exmidaclem  7293  exmidontriimlem4  7309  exmidontriim  7310  pw1on  7311  ccfunen  7349  cc2lem  7351  cc3  7353  acnccim  7357  genprndl  7607  genprndu  7608  nqprloc  7631  ltexprlemrnd  7691  ltexprlemdisj  7692  lteupri  7703  recexprlemrnd  7715  recexprlemdisj  7716  caucvgprlemlim  7767  caucvgprprlemlim  7797  suplocexprlemml  7802  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  caucvgsrlembound  7880  caucvgsrlemgt1  7881  caucvgsrlemoffgt1  7885  caucvgsr  7888  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  elrealeu  7915  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  negeu  8236  eqord1  8529  eqord2  8530  creur  9005  creui  9006  suprzclex  9443  supinfneg  9688  infsupneg  9689  infregelbex  9691  indstr2  9702  iooidg  10003  iccsupr  10060  icoshftf1o  10085  fznlem  10135  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  zsupssdc  10347  exbtwnzlemstep  10356  exbtwnzlemex  10358  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgtcl  10523  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  frecuzrdgfunlem  10530  frecuzrdgsuctlem  10534  nninfinf  10554  iseqovex  10569  seq3val  10571  seqvalcd  10572  seq3-1  10573  seqf  10575  seq3p1  10576  seqovcd  10578  seqp1cd  10581  seq3clss  10582  seq3fveq2  10586  seqfveq2g  10588  seqfveqg  10589  seq3fveq  10590  seq3feq  10591  seq3shft2  10592  seqshft2g  10593  monoord  10596  monoord2  10597  ser3mono  10598  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemqk  10618  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1oleml  10627  seq3f1o  10628  seqf1og  10632  seq3id3  10635  seq3id  10636  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  ser3ge0  10647  nn0ltexp2  10820  bccl  10878  hashinfuni  10888  hashennnuni  10890  wrdexg  10965  shftf  11014  seq3shft  11022  caucvgrelemcau  11164  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemcvg  11203  resqrexlemglsq  11206  resqrexlemga  11207  maxabslemval  11392  negfi  11412  minmax  11414  xrmaxiflemval  11434  xrminmax  11449  climconst  11474  2clim  11485  climcn1  11492  climcn2  11493  reccn2ap  11497  cn1lem  11498  climsqz  11519  climsqz2  11520  climcau  11531  climrecvg1n  11532  serf0  11536  sumeq2dv  11552  sumrbdclem  11561  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  zsumdc  11568  isum  11569  fsumgcl  11570  fsum3  11571  fsumf1o  11574  isumss  11575  fisumss  11576  isumss2  11577  fsum3cvg2  11578  fsumsersdc  11579  fsum3ser  11581  fsumcl2lem  11582  fsumadd  11590  fsumsplit  11591  fsumm1  11600  fsum1p  11602  isumclim3  11607  isummulc2  11610  sumsplitdc  11616  fsum2dlemstep  11618  fisumcom2  11622  fsumshftm  11629  fsummulc2  11632  fsumge1  11645  fsum00  11646  fsumabs  11649  telfsumo  11650  telfsumo2  11651  fsumparts  11654  fsumrelem  11655  fsumiun  11661  hashiun  11662  hash2iun  11663  binomlem  11667  isumshft  11674  isum1p  11676  isumnn0nn  11677  isumrpcl  11678  isumlessdc  11680  divcnv  11681  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemseq  11710  cvgratnnlemabsle  11711  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratnn  11715  cvgratz  11716  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  clim2prod  11723  prodeq2dv  11750  prodrbdclem  11755  fproddccvg  11756  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  iprodap  11764  fprodseq  11767  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodmul  11775  fprodsplit  11781  fprodm1  11782  fprod1p  11783  fprodm1s  11785  fprodp1s  11786  fprodunsn  11788  fprodcl2lem  11789  fprodabs  11800  fprodeq0  11801  fprodap0  11805  fprod2dlemstep  11806  fprodcom2fi  11810  fprodrec  11813  fprodmodd  11825  efcvgfsum  11851  dvdsssfz1  12036  bitsfi  12141  bitsinv1  12146  dvdsbnd  12150  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemle  12202  bezoutlemsup  12203  dfgcd3  12204  dfgcd2  12208  nnwodc  12230  uzwodc  12231  nnwosdc  12233  nninfctlemfo  12234  coprmgcdb  12283  prmdc  12325  isprm5  12337  isprm6  12342  phivalfi  12407  phibndlem  12411  dfphi2  12415  hashdvds  12416  phiprmpw  12417  phimullem  12420  eulerthlemfi  12423  dvdsfi  12434  hashgcdeq  12435  phisum  12436  reumodprminv  12449  pclemdc  12484  pc2dvds  12526  pcz  12528  pcprmpw2  12529  pcmptdvds  12541  pcprod  12542  pcfac  12546  qexpz  12548  prmpwdvds  12551  pockthg  12553  infpnlem2  12556  1arithlem4  12562  1arith  12563  4sqlemafi  12591  4sqlemffi  12592  4sqleminfi  12593  ennnfonelemex  12658  ennnfonelemfun  12661  ennnfonelemf1  12662  ennnfonelemnn0  12666  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  ctiunctlemudc  12681  ctiunctlemf  12682  ctiunctlemfo  12683  omctfn  12687  ssnnctlemct  12690  nninfdclemcl  12692  nninfdclemp1  12694  pwsbas  12996  imasival  13010  ismgmid2  13084  mgmidsssn0  13088  grpinvalem  13089  grpinva  13090  gsumress  13099  issgrpd  13116  prdsplusgsgrpcl  13118  sgrpidmndm  13124  ismndd  13141  mndpfo  13142  prdsplusgcl  13150  prdsidlem  13151  mhmima  13195  mhmeql  13196  gsumvallem2  13197  isgrpd2e  13224  dfgrp2  13231  grpidd2  13245  isgrpinv  13258  grplrinv  13261  grpidinv  13263  dfgrp3me  13304  prdsinvlem  13312  mhmmnd  13324  ghmgrp  13326  mulgsubcl  13344  issubg2m  13397  issubgrpd2  13398  grpissubg  13402  subgintm  13406  nmzsubg  13418  ssnmz  13419  ghmrn  13465  ghmeql  13475  ghmf1  13481  conjnmz  13487  conjnmzb  13488  rinvmod  13517  srgrz  13618  srglz  13619  srgisid  13620  ringsrg  13681  rhmdvdsr  13809  rhmopp  13810  subrngintm  13846  subrg1  13865  subrgugrp  13874  subrgintm  13877  unitrrg  13901  aprap  13920  islmodd  13927  lssuni  13997  lsssubg  14011  lssintclm  14018  dflidl2rng  14115  lidlsubg  14120  cnsubglem  14213  gsumfzfsumlemm  14221  znf1o  14285  znidomb  14292  psrbagfi  14307  psr1clfi  14322  mplsubgfilemm  14332  mplsubgfilemcl  14333  mplsubgfi  14335  fiinbas  14393  tgclb  14409  restbasg  14512  iscnp4  14562  cnco  14565  cnptopco  14566  cnss1  14570  cnss2  14571  cncnpi  14572  cncnp  14574  cnconst2  14577  cnrest  14579  cnptopresti  14582  cnpdis  14586  lmtopcnp  14594  txbasval  14611  tx1cn  14613  tx2cn  14614  txcnp  14615  upxp  14616  txdis1cn  14622  cnmpt11  14627  psmet0  14671  psmettri2  14672  psmetxrge0  14676  psmetres2  14677  ismeti  14690  xmetpsmet  14713  blsscls2  14837  comet  14843  xmettx  14854  tgioo  14898  tgqioo  14899  fsumcncntop  14911  elcncf1di  14923  cdivcncfap  14948  mulcncflem  14951  mulcncf  14952  cnopnap  14955  divcncfap  14958  dedekindeulemuub  14961  dedekindeulemlu  14965  suplociccreex  14968  suplociccex  14969  dedekindicclemuub  14970  dedekindicclemlu  14974  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemdisj  14984  ivthinclemloc  14985  ivthinc  14987  ivthdec  14988  dich0  14996  ivthdich  14997  cnplimclemr  15013  limccnp2cntop  15021  limccoap  15022  dvcn  15044  dvfre  15054  dvrecap  15057  dvmptclx  15062  dvmptaddx  15063  dvmptmulx  15064  dveflem  15070  dvef  15071  ply1termlem  15086  plyaddlem1  15091  plymullem1  15092  plycoeid3  15101  plycj  15105  plyreres  15108  dvply1  15109  sin0pilem1  15125  sin0pilem2  15126  mpodvdsmulf1o  15334  mersenne  15341  perfectlem2  15344  lgsval2lem  15359  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1f1o  15409  gausslemma2dlem2  15411  gausslemma2dlem3  15412  lgsquadlemofi  15425  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem1a1  15435  2sqlem6  15469  2sqlem8  15472  2sqlem10  15474  fnmptd  15558  bj-charfun  15561  bj-charfundc  15562  bj-charfunr  15564  2omap  15750  pw1nct  15758  nnsf  15760  nninfalllem1  15763  nninfall  15764  nninfself  15768  nninfsellemeq  15769  nninfsellemeqinf  15771  nninfsel  15772  nnnninfex  15777  nninfnfiinf  15778  isomninnlem  15787  trilpolemeq1  15797  trilpo  15800  apdiff  15805  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809  redcwlpo  15812  redc0  15814  reap0  15815  dceqnconst  15817  dcapnconst  15818  nconstwlpolem  15822  nconstwlpo  15823  neapmkv  15825  ltlenmkv  15827