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  2727  ssrabdv  3236  ss2rabdv  3238  iuneq2dv  3909  iunssd  3934  disjeq2dv  3987  mpteq12dva  4086  triun  4116  issod  4321  frirrg  4352  frind  4354  peano2  4596  dmmptd  5348  fun11iun  5484  fniinfv  5576  eqfnfv  5615  eqfnfvd  5618  fnmptfvd  5622  dff3im  5663  dffo4  5666  fmptd  5672  ffnfv  5676  fmpt2d  5680  ffvresb  5681  fconst2g  5733  fconstfvm  5736  resfunexg  5739  eufnfv  5749  foco2  5756  fniunfv  5765  fcofo  5787  fliftel  5796  fliftfun  5799  fliftfuns  5801  riota5f  5857  f1ocnvd  6075  suppssov1  6082  offval2  6100  ofrfval2  6101  offveqb  6104  caofref  6106  caofinvl  6107  opabex3d  6124  oprssdmm  6174  f1od2  6238  disjxp1  6239  tfrlem1  6311  tfrlemisucaccv  6328  tfrlemiubacc  6333  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemubacc  6349  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemubacc  6362  tfrcllemaccex  6364  tfrcllemres  6365  tfrcl  6367  rdgon  6389  freccllem  6405  frecfcllem  6407  omcl  6464  oeicl  6465  qliftfuns  6621  ixpeq2dva  6715  xpf1o  6846  mapxpen  6850  isinfinf  6899  fimax2gtrilemstep  6902  undifdcss  6924  eqsuptid  6998  eqinftid  7022  difinfsnlem  7100  difinfsn  7101  ctmlemr  7109  ctm  7110  ctssdclemn0  7111  ctssdccl  7112  enumctlemm  7115  nnnninf  7126  nnnninfeq  7128  enomnilem  7138  ismkvnex  7155  enmkvlem  7161  enwomnilem  7169  nninfwlporlemd  7172  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  nninfwlpoim  7178  acfun  7208  exmidaclem  7209  exmidontriimlem4  7225  exmidontriim  7226  pw1on  7227  ccfunen  7265  cc2lem  7267  cc3  7269  genprndl  7522  genprndu  7523  nqprloc  7546  ltexprlemrnd  7606  ltexprlemdisj  7607  lteupri  7618  recexprlemrnd  7630  recexprlemdisj  7631  caucvgprlemlim  7682  caucvgprprlemlim  7712  suplocexprlemml  7717  suplocexprlemrl  7718  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  caucvgsrlembound  7795  caucvgsrlemgt1  7796  caucvgsrlemoffgt1  7800  caucvgsr  7803  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  elrealeu  7830  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  negeu  8150  eqord1  8442  eqord2  8443  creur  8918  creui  8919  suprzclex  9353  supinfneg  9597  infsupneg  9598  infregelbex  9600  indstr2  9611  iooidg  9911  iccsupr  9968  icoshftf1o  9993  fznlem  10043  exfzdc  10242  exbtwnzlemstep  10250  exbtwnzlemex  10252  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgtcl  10414  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  frecuzrdgfunlem  10421  frecuzrdgsuctlem  10425  iseqovex  10458  seq3val  10460  seqvalcd  10461  seq3-1  10462  seqf  10463  seq3p1  10464  seqovcd  10465  seqp1cd  10468  seq3clss  10469  seq3fveq2  10471  seq3fveq  10473  seq3feq  10474  seq3shft2  10475  monoord  10478  monoord2  10479  ser3mono  10480  seq3split  10481  seq3caopr3  10483  seq3caopr2  10484  iseqf1olemqk  10496  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3f1oleml  10505  seq3f1o  10506  seq3id3  10509  seq3id  10510  seq3id2  10511  seq3homo  10512  seq3z  10513  ser3ge0  10519  nn0ltexp2  10691  bccl  10749  hashinfuni  10759  hashennnuni  10761  shftf  10841  seq3shft  10849  caucvgrelemcau  10991  cvg1nlemcau  10995  cvg1nlemres  10996  resqrexlemcvg  11030  resqrexlemglsq  11033  resqrexlemga  11034  maxabslemval  11219  negfi  11238  minmax  11240  xrmaxiflemval  11260  xrminmax  11275  climconst  11300  2clim  11311  climcn1  11318  climcn2  11319  reccn2ap  11323  cn1lem  11324  climsqz  11345  climsqz2  11346  climcau  11357  climrecvg1n  11358  serf0  11362  sumeq2dv  11378  sumrbdclem  11387  fsum3cvg  11388  summodclem3  11390  summodclem2a  11391  zsumdc  11394  isum  11395  fsumgcl  11396  fsum3  11397  fsumf1o  11400  isumss  11401  fisumss  11402  isumss2  11403  fsum3cvg2  11404  fsumsersdc  11405  fsum3ser  11407  fsumcl2lem  11408  fsumadd  11416  fsumsplit  11417  fsumm1  11426  fsum1p  11428  isumclim3  11433  isummulc2  11436  sumsplitdc  11442  fsum2dlemstep  11444  fisumcom2  11448  fsumshftm  11455  fsummulc2  11458  fsumge1  11471  fsum00  11472  fsumabs  11475  telfsumo  11476  telfsumo2  11477  fsumparts  11480  fsumrelem  11481  fsumiun  11487  hashiun  11488  hash2iun  11489  binomlem  11493  isumshft  11500  isum1p  11502  isumnn0nn  11503  isumrpcl  11504  isumlessdc  11506  divcnv  11507  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratnnlemseq  11536  cvgratnnlemabsle  11537  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratnn  11541  cvgratz  11542  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  clim2prod  11549  prodeq2dv  11576  prodrbdclem  11581  fproddccvg  11582  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  iprodap  11590  fprodseq  11593  fprodf1o  11598  prodssdc  11599  fprodssdc  11600  fprodmul  11601  fprodsplit  11607  fprodm1  11608  fprod1p  11609  fprodm1s  11611  fprodp1s  11612  fprodunsn  11614  fprodcl2lem  11615  fprodabs  11626  fprodeq0  11627  fprodap0  11631  fprod2dlemstep  11632  fprodcom2fi  11636  fprodrec  11639  fprodmodd  11651  efcvgfsum  11677  dvdsssfz1  11860  zsupcllemstep  11948  infssuzex  11952  suprzubdc  11955  zsupssdc  11957  dvdsbnd  11959  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlemle  12011  bezoutlemsup  12012  dfgcd3  12013  dfgcd2  12017  nnwodc  12039  uzwodc  12040  nnwosdc  12042  coprmgcdb  12090  prmdc  12132  isprm5  12144  isprm6  12149  phivalfi  12214  phibndlem  12218  dfphi2  12222  hashdvds  12223  phiprmpw  12224  phimullem  12227  eulerthlemfi  12230  hashgcdeq  12241  phisum  12242  reumodprminv  12255  pclemdc  12290  pc2dvds  12331  pcz  12333  pcprmpw2  12334  pcmptdvds  12345  pcprod  12346  pcfac  12350  qexpz  12352  prmpwdvds  12355  pockthg  12357  infpnlem2  12360  1arithlem4  12366  1arith  12367  ennnfonelemex  12417  ennnfonelemfun  12420  ennnfonelemf1  12421  ennnfonelemnn0  12425  ennnfonelemim  12427  exmidunben  12429  ctinfomlemom  12430  ctinfom  12431  ctinf  12433  ctiunctlemudc  12440  ctiunctlemf  12441  ctiunctlemfo  12442  omctfn  12446  ssnnctlemct  12449  nninfdclemcl  12451  nninfdclemp1  12453  imasival  12732  ismgmid2  12804  mgmidsssn0  12808  grprinvlem  12809  grprinvd  12810  sgrpidmndm  12826  ismndd  12843  mndpfo  12844  mhmima  12880  mhmeql  12881  isgrpd2e  12901  dfgrp2  12907  grpidd2  12919  isgrpinv  12931  grplrinv  12932  grpidinv  12934  dfgrp3me  12975  mhmmnd  12985  ghmgrp  12987  mulgsubcl  13002  issubg2m  13054  issubgrpd2  13055  grpissubg  13059  subgintm  13063  nmzsubg  13075  ssnmz  13076  rinvmod  13117  srgrz  13172  srglz  13173  srgisid  13174  ringsrg  13229  subrg1  13357  subrgugrp  13366  subrgintm  13369  aprap  13381  islmodd  13388  lssuni  13455  lsssubg  13469  lssintclm  13476  cnsubglem  13512  fiinbas  13588  tgclb  13604  restbasg  13707  iscnp4  13757  cnco  13760  cnptopco  13761  cnss1  13765  cnss2  13766  cncnpi  13767  cncnp  13769  cnconst2  13772  cnrest  13774  cnptopresti  13777  cnpdis  13781  lmtopcnp  13789  txbasval  13806  tx1cn  13808  tx2cn  13809  txcnp  13810  upxp  13811  txdis1cn  13817  cnmpt11  13822  psmet0  13866  psmettri2  13867  psmetxrge0  13871  psmetres2  13872  ismeti  13885  xmetpsmet  13908  blsscls2  14032  comet  14038  xmettx  14049  tgioo  14085  tgqioo  14086  fsumcncntop  14095  elcncf1di  14105  cdivcncfap  14126  mulcncflem  14129  mulcncf  14130  cnopnap  14133  dedekindeulemuub  14134  dedekindeulemlu  14138  suplociccreex  14141  suplociccex  14142  dedekindicclemuub  14143  dedekindicclemlu  14147  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemdisj  14157  ivthinclemloc  14158  ivthinc  14160  ivthdec  14161  cnplimclemr  14177  limccnp2cntop  14185  limccoap  14186  dvcn  14203  dvfre  14213  dvrecap  14216  dvmptclx  14219  dvmptaddx  14220  dvmptmulx  14221  dveflem  14226  dvef  14227  sin0pilem1  14241  sin0pilem2  14242  lgsval2lem  14450  lgsdirnn0  14487  lgsdinn0  14488  2sqlem6  14506  2sqlem8  14509  2sqlem10  14511  fnmptd  14595  bj-charfun  14598  bj-charfundc  14599  bj-charfunr  14601  pw1nct  14791  nnsf  14793  nninfalllem1  14796  nninfall  14797  nninfself  14801  nninfsellemeq  14802  nninfsellemeqinf  14804  nninfsel  14805  isomninnlem  14817  trilpolemeq1  14827  trilpo  14830  apdiff  14835  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839  redcwlpo  14842  redc0  14844  reap0  14845  dceqnconst  14847  dcapnconst  14848  nconstwlpolem  14852  nconstwlpo  14853  neapmkv  14855  ltlenmkv  14857