Theorem ralrimiva 2543

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 114	. 2 |- ( ph -> ( x e. A -> ps ) )
3	2	ralrimiv 2542	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2141   A.wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  ralrimivvva  2553  rgen2  2556  rgen3  2557  nrexdv  2563  r19.29vva  2615  rabbidva  2718  ssrabdv  3226  ss2rabdv  3228  iuneq2dv  3894  disjeq2dv  3971  mpteq12dva  4070  triun  4100  issod  4304  frirrg  4335  frind  4337  peano2  4579  dmmptd  5328  fun11iun  5463  fniinfv  5554  eqfnfv  5593  eqfnfvd  5596  fnmptfvd  5600  dff3im  5641  dffo4  5644  fmptd  5650  ffnfv  5654  fmpt2d  5658  ffvresb  5659  fconst2g  5711  fconstfvm  5714  resfunexg  5717  eufnfv  5726  foco2  5733  fniunfv  5741  fcofo  5763  fliftel  5772  fliftfun  5775  fliftfuns  5777  riota5f  5833  f1ocnvd  6051  suppssov1  6058  offval2  6076  ofrfval2  6077  offveqb  6080  caofref  6082  caofinvl  6083  opabex3d  6100  oprssdmm  6150  f1od2  6214  disjxp1  6215  tfrlem1  6287  tfrlemisucaccv  6304  tfrlemiubacc  6309  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemubacc  6325  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemubacc  6338  tfrcllemaccex  6340  tfrcllemres  6341  tfrcl  6343  rdgon  6365  freccllem  6381  frecfcllem  6383  omcl  6440  oeicl  6441  qliftfuns  6597  ixpeq2dva  6691  xpf1o  6822  mapxpen  6826  isinfinf  6875  fimax2gtrilemstep  6878  undifdcss  6900  eqsuptid  6974  eqinftid  6998  difinfsnlem  7076  difinfsn  7077  ctmlemr  7085  ctm  7086  ctssdclemn0  7087  ctssdccl  7088  enumctlemm  7091  nnnninf  7102  nnnninfeq  7104  enomnilem  7114  ismkvnex  7131  enmkvlem  7137  enwomnilem  7145  nninfwlporlemd  7148  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  nninfwlpoim  7154  acfun  7184  exmidaclem  7185  exmidontriimlem4  7201  exmidontriim  7202  pw1on  7203  ccfunen  7226  cc2lem  7228  cc3  7230  genprndl  7483  genprndu  7484  nqprloc  7507  ltexprlemrnd  7567  ltexprlemdisj  7568  lteupri  7579  recexprlemrnd  7591  recexprlemdisj  7592  caucvgprlemlim  7643  caucvgprprlemlim  7673  suplocexprlemml  7678  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  caucvgsrlembound  7756  caucvgsrlemgt1  7757  caucvgsrlemoffgt1  7761  caucvgsr  7764  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  elrealeu  7791  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  negeu  8110  eqord1  8402  eqord2  8403  creur  8875  creui  8876  suprzclex  9310  supinfneg  9554  infsupneg  9555  infregelbex  9557  indstr2  9568  iooidg  9866  iccsupr  9923  icoshftf1o  9948  fznlem  9997  exfzdc  10196  exbtwnzlemstep  10204  exbtwnzlemex  10206  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgtcl  10368  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgfunlem  10375  frecuzrdgsuctlem  10379  iseqovex  10412  seq3val  10414  seqvalcd  10415  seq3-1  10416  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  seq3clss  10423  seq3fveq2  10425  seq3fveq  10427  seq3feq  10428  seq3shft2  10429  monoord  10432  monoord2  10433  ser3mono  10434  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  iseqf1olemqk  10450  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1oleml  10459  seq3f1o  10460  seq3id3  10463  seq3id  10464  seq3id2  10465  seq3homo  10466  seq3z  10467  ser3ge0  10473  nn0ltexp2  10644  bccl  10701  hashinfuni  10711  hashennnuni  10713  shftf  10794  seq3shft  10802  caucvgrelemcau  10944  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemcvg  10983  resqrexlemglsq  10986  resqrexlemga  10987  maxabslemval  11172  negfi  11191  minmax  11193  xrmaxiflemval  11213  xrminmax  11228  climconst  11253  2clim  11264  climcn1  11271  climcn2  11272  reccn2ap  11276  cn1lem  11277  climsqz  11298  climsqz2  11299  climcau  11310  climrecvg1n  11311  serf0  11315  sumeq2dv  11331  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  zsumdc  11347  isum  11348  fsumgcl  11349  fsum3  11350  fsumf1o  11353  isumss  11354  fisumss  11355  isumss2  11356  fsum3cvg2  11357  fsumsersdc  11358  fsum3ser  11360  fsumcl2lem  11361  fsumadd  11369  fsumsplit  11370  fsumm1  11379  fsum1p  11381  isumclim3  11386  isummulc2  11389  sumsplitdc  11395  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fsummulc2  11411  fsumge1  11424  fsum00  11425  fsumabs  11428  telfsumo  11429  telfsumo2  11430  fsumparts  11433  fsumrelem  11434  fsumiun  11440  hashiun  11441  hash2iun  11442  binomlem  11446  isumshft  11453  isum1p  11455  isumnn0nn  11456  isumrpcl  11457  isumlessdc  11459  divcnv  11460  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemseq  11489  cvgratnnlemabsle  11490  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratnn  11494  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  clim2prod  11502  prodeq2dv  11529  prodrbdclem  11534  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  iprodap  11543  fprodseq  11546  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodmul  11554  fprodsplit  11560  fprodm1  11561  fprod1p  11562  fprodm1s  11564  fprodp1s  11565  fprodunsn  11567  fprodcl2lem  11568  fprodabs  11579  fprodeq0  11580  fprodap0  11584  fprod2dlemstep  11585  fprodcom2fi  11589  fprodrec  11592  fprodmodd  11604  efcvgfsum  11630  dvdsssfz1  11812  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  zsupssdc  11909  dvdsbnd  11911  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemle  11963  bezoutlemsup  11964  dfgcd3  11965  dfgcd2  11969  nnwodc  11991  uzwodc  11992  nnwosdc  11994  coprmgcdb  12042  prmdc  12084  isprm5  12096  isprm6  12101  phivalfi  12166  phibndlem  12170  dfphi2  12174  hashdvds  12175  phiprmpw  12176  phimullem  12179  eulerthlemfi  12182  hashgcdeq  12193  phisum  12194  reumodprminv  12207  pclemdc  12242  pc2dvds  12283  pcz  12285  pcprmpw2  12286  pcmptdvds  12297  pcprod  12298  pcfac  12302  qexpz  12304  prmpwdvds  12307  pockthg  12309  infpnlem2  12312  1arithlem4  12318  1arith  12319  ennnfonelemex  12369  ennnfonelemfun  12372  ennnfonelemf1  12373  ennnfonelemnn0  12377  ennnfonelemim  12379  exmidunben  12381  ctinfomlemom  12382  ctinfom  12383  ctinf  12385  ctiunctlemudc  12392  ctiunctlemf  12393  ctiunctlemfo  12394  omctfn  12398  ssnnctlemct  12401  nninfdclemcl  12403  nninfdclemp1  12405  ismgmid2  12634  mgmidsssn0  12638  grprinvlem  12639  grprinvd  12640  sgrpidmndm  12656  ismndd  12673  mndpfo  12674  mhmima  12706  mhmeql  12707  isgrpd2e  12726  dfgrp2  12732  grpidd2  12744  isgrpinv  12756  grplrinv  12757  grpidinv  12759  fiinbas  12841  tgclb  12859  restbasg  12962  iscnp4  13012  cnco  13015  cnptopco  13016  cnss1  13020  cnss2  13021  cncnpi  13022  cncnp  13024  cnconst2  13027  cnrest  13029  cnptopresti  13032  cnpdis  13036  lmtopcnp  13044  txbasval  13061  tx1cn  13063  tx2cn  13064  txcnp  13065  upxp  13066  txdis1cn  13072  cnmpt11  13077  psmet0  13121  psmettri2  13122  psmetxrge0  13126  psmetres2  13127  ismeti  13140  xmetpsmet  13163  blsscls2  13287  comet  13293  xmettx  13304  tgioo  13340  tgqioo  13341  fsumcncntop  13350  elcncf1di  13360  cdivcncfap  13381  mulcncflem  13384  mulcncf  13385  cnopnap  13388  dedekindeulemuub  13389  dedekindeulemlu  13393  suplociccreex  13396  suplociccex  13397  dedekindicclemuub  13398  dedekindicclemlu  13402  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemdisj  13412  ivthinclemloc  13413  ivthinc  13415  ivthdec  13416  cnplimclemr  13432  limccnp2cntop  13440  limccoap  13441  dvcn  13458  dvfre  13468  dvrecap  13471  dvmptclx  13474  dvmptaddx  13475  dvmptmulx  13476  dveflem  13481  dvef  13482  sin0pilem1  13496  sin0pilem2  13497  lgsval2lem  13705  lgsdirnn0  13742  lgsdinn0  13743  2sqlem6  13750  2sqlem8  13753  2sqlem10  13755  fnmptd  13839  bj-charfun  13842  bj-charfundc  13843  bj-charfunr  13845  pw1nct  14036  nnsf  14038  nninfalllem1  14041  nninfall  14042  nninfself  14046  nninfsellemeq  14047  nninfsellemeqinf  14049  nninfsel  14050  isomninnlem  14062  trilpolemeq1  14072  trilpo  14075  apdiff  14080  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  redcwlpo  14087  redc0  14089  reap0  14090  dceqnconst  14091  dcapnconst  14092  nconstwlpolem  14096  nconstwlpo  14097  neapmkv  14099