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  3906  disjeq2dv  3983  mpteq12dva  4082  triun  4112  issod  4317  frirrg  4348  frind  4350  peano2  4592  dmmptd  5343  fun11iun  5479  fniinfv  5571  eqfnfv  5610  eqfnfvd  5613  fnmptfvd  5617  dff3im  5658  dffo4  5661  fmptd  5667  ffnfv  5671  fmpt2d  5675  ffvresb  5676  fconst2g  5728  fconstfvm  5731  resfunexg  5734  eufnfv  5743  foco2  5750  fniunfv  5758  fcofo  5780  fliftel  5789  fliftfun  5792  fliftfuns  5794  riota5f  5850  f1ocnvd  6068  suppssov1  6075  offval2  6093  ofrfval2  6094  offveqb  6097  caofref  6099  caofinvl  6100  opabex3d  6117  oprssdmm  6167  f1od2  6231  disjxp1  6232  tfrlem1  6304  tfrlemisucaccv  6321  tfrlemiubacc  6326  tfr1onlemsucfn  6336  tfr1onlemsucaccv  6337  tfr1onlembxssdm  6339  tfr1onlembfn  6340  tfr1onlemubacc  6342  tfr1onlemaccex  6344  tfr1onlemres  6345  tfrcllemsucfn  6349  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  tfrcllembfn  6353  tfrcllemubacc  6355  tfrcllemaccex  6357  tfrcllemres  6358  tfrcl  6360  rdgon  6382  freccllem  6398  frecfcllem  6400  omcl  6457  oeicl  6458  qliftfuns  6614  ixpeq2dva  6708  xpf1o  6839  mapxpen  6843  isinfinf  6892  fimax2gtrilemstep  6895  undifdcss  6917  eqsuptid  6991  eqinftid  7015  difinfsnlem  7093  difinfsn  7094  ctmlemr  7102  ctm  7103  ctssdclemn0  7104  ctssdccl  7105  enumctlemm  7108  nnnninf  7119  nnnninfeq  7121  enomnilem  7131  ismkvnex  7148  enmkvlem  7154  enwomnilem  7162  nninfwlporlemd  7165  nninfwlpoimlemg  7168  nninfwlpoimlemginf  7169  nninfwlpoim  7171  acfun  7201  exmidaclem  7202  exmidontriimlem4  7218  exmidontriim  7219  pw1on  7220  ccfunen  7258  cc2lem  7260  cc3  7262  genprndl  7515  genprndu  7516  nqprloc  7539  ltexprlemrnd  7599  ltexprlemdisj  7600  lteupri  7611  recexprlemrnd  7623  recexprlemdisj  7624  caucvgprlemlim  7675  caucvgprprlemlim  7705  suplocexprlemml  7710  suplocexprlemrl  7711  suplocexprlemmu  7712  suplocexprlemru  7713  suplocexprlemdisj  7714  suplocexprlemloc  7715  suplocexprlemub  7717  caucvgsrlembound  7788  caucvgsrlemgt1  7789  caucvgsrlemoffgt1  7793  caucvgsr  7796  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  elrealeu  7823  axcaucvglemcau  7892  axcaucvglemres  7893  axpre-suploclemres  7895  negeu  8142  eqord1  8434  eqord2  8435  creur  8910  creui  8911  suprzclex  9345  supinfneg  9589  infsupneg  9590  infregelbex  9592  indstr2  9603  iooidg  9903  iccsupr  9960  icoshftf1o  9985  fznlem  10034  exfzdc  10233  exbtwnzlemstep  10241  exbtwnzlemex  10243  frec2uzrdg  10402  frecuzrdgrcl  10403  frecuzrdgtcl  10405  frecuzrdgsuc  10407  frecuzrdgrclt  10408  frecuzrdgg  10409  frecuzrdgfunlem  10412  frecuzrdgsuctlem  10416  iseqovex  10449  seq3val  10451  seqvalcd  10452  seq3-1  10453  seqf  10454  seq3p1  10455  seqovcd  10456  seqp1cd  10459  seq3clss  10460  seq3fveq2  10462  seq3fveq  10464  seq3feq  10465  seq3shft2  10466  monoord  10469  monoord2  10470  ser3mono  10471  seq3split  10472  seq3caopr3  10474  seq3caopr2  10475  iseqf1olemqk  10487  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  iseqf1olemfvp  10490  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3f1olemqsum  10493  seq3f1oleml  10496  seq3f1o  10497  seq3id3  10500  seq3id  10501  seq3id2  10502  seq3homo  10503  seq3z  10504  ser3ge0  10510  nn0ltexp2  10681  bccl  10738  hashinfuni  10748  hashennnuni  10750  shftf  10830  seq3shft  10838  caucvgrelemcau  10980  cvg1nlemcau  10984  cvg1nlemres  10985  resqrexlemcvg  11019  resqrexlemglsq  11022  resqrexlemga  11023  maxabslemval  11208  negfi  11227  minmax  11229  xrmaxiflemval  11249  xrminmax  11264  climconst  11289  2clim  11300  climcn1  11307  climcn2  11308  reccn2ap  11312  cn1lem  11313  climsqz  11334  climsqz2  11335  climcau  11346  climrecvg1n  11347  serf0  11351  sumeq2dv  11367  sumrbdclem  11376  fsum3cvg  11377  summodclem3  11379  summodclem2a  11380  zsumdc  11383  isum  11384  fsumgcl  11385  fsum3  11386  fsumf1o  11389  isumss  11390  fisumss  11391  isumss2  11392  fsum3cvg2  11393  fsumsersdc  11394  fsum3ser  11396  fsumcl2lem  11397  fsumadd  11405  fsumsplit  11406  fsumm1  11415  fsum1p  11417  isumclim3  11422  isummulc2  11425  sumsplitdc  11431  fsum2dlemstep  11433  fisumcom2  11437  fsumshftm  11444  fsummulc2  11447  fsumge1  11460  fsum00  11461  fsumabs  11464  telfsumo  11465  telfsumo2  11466  fsumparts  11469  fsumrelem  11470  fsumiun  11476  hashiun  11477  hash2iun  11478  binomlem  11482  isumshft  11489  isum1p  11491  isumnn0nn  11492  isumrpcl  11493  isumlessdc  11495  divcnv  11496  cvgratnnlemnexp  11523  cvgratnnlemmn  11524  cvgratnnlemseq  11525  cvgratnnlemabsle  11526  cvgratnnlemfm  11528  cvgratnnlemrate  11529  cvgratnn  11530  cvgratz  11531  mertenslemi1  11534  mertenslem2  11535  mertensabs  11536  clim2prod  11538  prodeq2dv  11565  prodrbdclem  11570  fproddccvg  11571  prodmodclem3  11574  prodmodclem2a  11575  zproddc  11578  iprodap  11579  fprodseq  11582  fprodf1o  11587  prodssdc  11588  fprodssdc  11589  fprodmul  11590  fprodsplit  11596  fprodm1  11597  fprod1p  11598  fprodm1s  11600  fprodp1s  11601  fprodunsn  11603  fprodcl2lem  11604  fprodabs  11615  fprodeq0  11616  fprodap0  11620  fprod2dlemstep  11621  fprodcom2fi  11625  fprodrec  11628  fprodmodd  11640  efcvgfsum  11666  dvdsssfz1  11848  zsupcllemstep  11936  infssuzex  11940  suprzubdc  11943  zsupssdc  11945  dvdsbnd  11947  bezoutlemstep  11988  bezoutlemmain  11989  bezoutlemle  11999  bezoutlemsup  12000  dfgcd3  12001  dfgcd2  12005  nnwodc  12027  uzwodc  12028  nnwosdc  12030  coprmgcdb  12078  prmdc  12120  isprm5  12132  isprm6  12137  phivalfi  12202  phibndlem  12206  dfphi2  12210  hashdvds  12211  phiprmpw  12212  phimullem  12215  eulerthlemfi  12218  hashgcdeq  12229  phisum  12230  reumodprminv  12243  pclemdc  12278  pc2dvds  12319  pcz  12321  pcprmpw2  12322  pcmptdvds  12333  pcprod  12334  pcfac  12338  qexpz  12340  prmpwdvds  12343  pockthg  12345  infpnlem2  12348  1arithlem4  12354  1arith  12355  ennnfonelemex  12405  ennnfonelemfun  12408  ennnfonelemf1  12409  ennnfonelemnn0  12413  ennnfonelemim  12415  exmidunben  12417  ctinfomlemom  12418  ctinfom  12419  ctinf  12421  ctiunctlemudc  12428  ctiunctlemf  12429  ctiunctlemfo  12430  omctfn  12434  ssnnctlemct  12437  nninfdclemcl  12439  nninfdclemp1  12441  ismgmid2  12729  mgmidsssn0  12733  grprinvlem  12734  grprinvd  12735  sgrpidmndm  12751  ismndd  12768  mndpfo  12769  mhmima  12803  mhmeql  12804  isgrpd2e  12824  dfgrp2  12830  grpidd2  12842  isgrpinv  12854  grplrinv  12855  grpidinv  12857  dfgrp3me  12898  mhmmnd  12908  ghmgrp  12910  mulgsubcl  12925  issubg2m  12975  issubgrpd2  12976  grpissubg  12980  subgintm  12984  rinvmod  13012  srgrz  13067  srglz  13068  srgisid  13069  ringsrg  13124  aprap  13243  fiinbas  13329  tgclb  13347  restbasg  13450  iscnp4  13500  cnco  13503  cnptopco  13504  cnss1  13508  cnss2  13509  cncnpi  13510  cncnp  13512  cnconst2  13515  cnrest  13517  cnptopresti  13520  cnpdis  13524  lmtopcnp  13532  txbasval  13549  tx1cn  13551  tx2cn  13552  txcnp  13553  upxp  13554  txdis1cn  13560  cnmpt11  13565  psmet0  13609  psmettri2  13610  psmetxrge0  13614  psmetres2  13615  ismeti  13628  xmetpsmet  13651  blsscls2  13775  comet  13781  xmettx  13792  tgioo  13828  tgqioo  13829  fsumcncntop  13838  elcncf1di  13848  cdivcncfap  13869  mulcncflem  13872  mulcncf  13873  cnopnap  13876  dedekindeulemuub  13877  dedekindeulemlu  13881  suplociccreex  13884  suplociccex  13885  dedekindicclemuub  13886  dedekindicclemlu  13890  ivthinclemlopn  13896  ivthinclemlr  13897  ivthinclemuopn  13898  ivthinclemur  13899  ivthinclemdisj  13900  ivthinclemloc  13901  ivthinc  13903  ivthdec  13904  cnplimclemr  13920  limccnp2cntop  13928  limccoap  13929  dvcn  13946  dvfre  13956  dvrecap  13959  dvmptclx  13962  dvmptaddx  13963  dvmptmulx  13964  dveflem  13969  dvef  13970  sin0pilem1  13984  sin0pilem2  13985  lgsval2lem  14193  lgsdirnn0  14230  lgsdinn0  14231  2sqlem6  14238  2sqlem8  14241  2sqlem10  14243  fnmptd  14327  bj-charfun  14330  bj-charfundc  14331  bj-charfunr  14333  pw1nct  14523  nnsf  14525  nninfalllem1  14528  nninfall  14529  nninfself  14533  nninfsellemeq  14534  nninfsellemeqinf  14536  nninfsel  14537  isomninnlem  14549  trilpolemeq1  14559  trilpo  14562  apdiff  14567  iswomninnlem  14568  iswomni0  14570  ismkvnnlem  14571  redcwlpo  14574  redc0  14576  reap0  14577  dceqnconst  14578  dcapnconst  14579  nconstwlpolem  14583  nconstwlpo  14584  neapmkv  14586  ltlenmkv  14588