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  7253  finacn  7287  acfun  7290  exmidaclem  7291  exmidontriimlem4  7307  exmidontriim  7308  pw1on  7309  ccfunen  7347  cc2lem  7349  cc3  7351  acnccim  7355  genprndl  7605  genprndu  7606  nqprloc  7629  ltexprlemrnd  7689  ltexprlemdisj  7690  lteupri  7701  recexprlemrnd  7713  recexprlemdisj  7714  caucvgprlemlim  7765  caucvgprprlemlim  7795  suplocexprlemml  7800  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  caucvgsrlembound  7878  caucvgsrlemgt1  7879  caucvgsrlemoffgt1  7883  caucvgsr  7886  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  elrealeu  7913  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  negeu  8234  eqord1  8527  eqord2  8528  creur  9003  creui  9004  suprzclex  9441  supinfneg  9686  infsupneg  9687  infregelbex  9689  indstr2  9700  iooidg  10001  iccsupr  10058  icoshftf1o  10083  fznlem  10133  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  suprzubdc  10343  zsupssdc  10345  exbtwnzlemstep  10354  exbtwnzlemex  10356  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgtcl  10521  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgfunlem  10528  frecuzrdgsuctlem  10532  nninfinf  10552  iseqovex  10567  seq3val  10569  seqvalcd  10570  seq3-1  10571  seqf  10573  seq3p1  10574  seqovcd  10576  seqp1cd  10579  seq3clss  10580  seq3fveq2  10584  seqfveq2g  10586  seqfveqg  10587  seq3fveq  10588  seq3feq  10589  seq3shft2  10590  seqshft2g  10591  monoord  10594  monoord2  10595  ser3mono  10596  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemqk  10616  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1oleml  10625  seq3f1o  10626  seqf1og  10630  seq3id3  10633  seq3id  10634  seq3id2  10635  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  ser3ge0  10645  nn0ltexp2  10818  bccl  10876  hashinfuni  10886  hashennnuni  10888  wrdexg  10963  shftf  11012  seq3shft  11020  caucvgrelemcau  11162  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemcvg  11201  resqrexlemglsq  11204  resqrexlemga  11205  maxabslemval  11390  negfi  11410  minmax  11412  xrmaxiflemval  11432  xrminmax  11447  climconst  11472  2clim  11483  climcn1  11490  climcn2  11491  reccn2ap  11495  cn1lem  11496  climsqz  11517  climsqz2  11518  climcau  11529  climrecvg1n  11530  serf0  11534  sumeq2dv  11550  sumrbdclem  11559  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  zsumdc  11566  isum  11567  fsumgcl  11568  fsum3  11569  fsumf1o  11572  isumss  11573  fisumss  11574  isumss2  11575  fsum3cvg2  11576  fsumsersdc  11577  fsum3ser  11579  fsumcl2lem  11580  fsumadd  11588  fsumsplit  11589  fsumm1  11598  fsum1p  11600  isumclim3  11605  isummulc2  11608  sumsplitdc  11614  fsum2dlemstep  11616  fisumcom2  11620  fsumshftm  11627  fsummulc2  11630  fsumge1  11643  fsum00  11644  fsumabs  11647  telfsumo  11648  telfsumo2  11649  fsumparts  11652  fsumrelem  11653  fsumiun  11659  hashiun  11660  hash2iun  11661  binomlem  11665  isumshft  11672  isum1p  11674  isumnn0nn  11675  isumrpcl  11676  isumlessdc  11678  divcnv  11679  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemseq  11708  cvgratnnlemabsle  11709  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratnn  11713  cvgratz  11714  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  clim2prod  11721  prodeq2dv  11748  prodrbdclem  11753  fproddccvg  11754  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  iprodap  11762  fprodseq  11765  fprodf1o  11770  prodssdc  11771  fprodssdc  11772  fprodmul  11773  fprodsplit  11779  fprodm1  11780  fprod1p  11781  fprodm1s  11783  fprodp1s  11784  fprodunsn  11786  fprodcl2lem  11787  fprodabs  11798  fprodeq0  11799  fprodap0  11803  fprod2dlemstep  11804  fprodcom2fi  11808  fprodrec  11811  fprodmodd  11823  efcvgfsum  11849  dvdsssfz1  12034  bitsfi  12139  bitsinv1  12144  dvdsbnd  12148  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemle  12200  bezoutlemsup  12201  dfgcd3  12202  dfgcd2  12206  nnwodc  12228  uzwodc  12229  nnwosdc  12231  nninfctlemfo  12232  coprmgcdb  12281  prmdc  12323  isprm5  12335  isprm6  12340  phivalfi  12405  phibndlem  12409  dfphi2  12413  hashdvds  12414  phiprmpw  12415  phimullem  12418  eulerthlemfi  12421  dvdsfi  12432  hashgcdeq  12433  phisum  12434  reumodprminv  12447  pclemdc  12482  pc2dvds  12524  pcz  12526  pcprmpw2  12527  pcmptdvds  12539  pcprod  12540  pcfac  12544  qexpz  12546  prmpwdvds  12549  pockthg  12551  infpnlem2  12554  1arithlem4  12560  1arith  12561  4sqlemafi  12589  4sqlemffi  12590  4sqleminfi  12591  ennnfonelemex  12656  ennnfonelemfun  12659  ennnfonelemf1  12660  ennnfonelemnn0  12664  ennnfonelemim  12666  exmidunben  12668  ctinfomlemom  12669  ctinfom  12670  ctinf  12672  ctiunctlemudc  12679  ctiunctlemf  12680  ctiunctlemfo  12681  omctfn  12685  ssnnctlemct  12688  nninfdclemcl  12690  nninfdclemp1  12692  pwsbas  12994  imasival  13008  ismgmid2  13082  mgmidsssn0  13086  grpinvalem  13087  grpinva  13088  gsumress  13097  issgrpd  13114  prdsplusgsgrpcl  13116  sgrpidmndm  13122  ismndd  13139  mndpfo  13140  prdsplusgcl  13148  prdsidlem  13149  mhmima  13193  mhmeql  13194  gsumvallem2  13195  isgrpd2e  13222  dfgrp2  13229  grpidd2  13243  isgrpinv  13256  grplrinv  13259  grpidinv  13261  dfgrp3me  13302  prdsinvlem  13310  mhmmnd  13322  ghmgrp  13324  mulgsubcl  13342  issubg2m  13395  issubgrpd2  13396  grpissubg  13400  subgintm  13404  nmzsubg  13416  ssnmz  13417  ghmrn  13463  ghmeql  13473  ghmf1  13479  conjnmz  13485  conjnmzb  13486  rinvmod  13515  srgrz  13616  srglz  13617  srgisid  13618  ringsrg  13679  rhmdvdsr  13807  rhmopp  13808  subrngintm  13844  subrg1  13863  subrgugrp  13872  subrgintm  13875  unitrrg  13899  aprap  13918  islmodd  13925  lssuni  13995  lsssubg  14009  lssintclm  14016  dflidl2rng  14113  lidlsubg  14118  cnsubglem  14211  gsumfzfsumlemm  14219  znf1o  14283  znidomb  14290  psr1clfi  14316  fiinbas  14369  tgclb  14385  restbasg  14488  iscnp4  14538  cnco  14541  cnptopco  14542  cnss1  14546  cnss2  14547  cncnpi  14548  cncnp  14550  cnconst2  14553  cnrest  14555  cnptopresti  14558  cnpdis  14562  lmtopcnp  14570  txbasval  14587  tx1cn  14589  tx2cn  14590  txcnp  14591  upxp  14592  txdis1cn  14598  cnmpt11  14603  psmet0  14647  psmettri2  14648  psmetxrge0  14652  psmetres2  14653  ismeti  14666  xmetpsmet  14689  blsscls2  14813  comet  14819  xmettx  14830  tgioo  14874  tgqioo  14875  fsumcncntop  14887  elcncf1di  14899  cdivcncfap  14924  mulcncflem  14927  mulcncf  14928  cnopnap  14931  divcncfap  14934  dedekindeulemuub  14937  dedekindeulemlu  14941  suplociccreex  14944  suplociccex  14945  dedekindicclemuub  14946  dedekindicclemlu  14950  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemdisj  14960  ivthinclemloc  14961  ivthinc  14963  ivthdec  14964  dich0  14972  ivthdich  14973  cnplimclemr  14989  limccnp2cntop  14997  limccoap  14998  dvcn  15020  dvfre  15030  dvrecap  15033  dvmptclx  15038  dvmptaddx  15039  dvmptmulx  15040  dveflem  15046  dvef  15047  ply1termlem  15062  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077  plycj  15081  plyreres  15084  dvply1  15085  sin0pilem1  15101  sin0pilem2  15102  mpodvdsmulf1o  15310  mersenne  15317  perfectlem2  15320  lgsval2lem  15335  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1f1o  15385  gausslemma2dlem2  15387  gausslemma2dlem3  15388  lgsquadlemofi  15401  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1a1  15411  2sqlem6  15445  2sqlem8  15448  2sqlem10  15450  fnmptd  15534  bj-charfun  15537  bj-charfundc  15538  bj-charfunr  15540  2omap  15726  pw1nct  15734  nnsf  15736  nninfalllem1  15739  nninfall  15740  nninfself  15744  nninfsellemeq  15745  nninfsellemeqinf  15747  nninfsel  15748  isomninnlem  15761  trilpolemeq1  15771  trilpo  15774  apdiff  15779  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  redcwlpo  15786  redc0  15788  reap0  15789  dceqnconst  15791  dcapnconst  15792  nconstwlpolem  15796  nconstwlpo  15797  neapmkv  15799  ltlenmkv  15801