Theorem ralrimiva 2539

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 2538	1 |- ( ph -> A. x e. A ps )

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  ralrimivvva  2549  rgen2  2552  rgen3  2553  nrexdv  2559  r19.29vva  2611  rabbidva  2714  ssrabdv  3221  ss2rabdv  3223  iuneq2dv  3887  disjeq2dv  3964  mpteq12dva  4063  triun  4093  issod  4297  frirrg  4328  frind  4330  peano2  4572  dmmptd  5318  fun11iun  5453  fniinfv  5544  eqfnfv  5583  eqfnfvd  5586  dff3im  5630  dffo4  5633  fmptd  5639  ffnfv  5643  fmpt2d  5647  ffvresb  5648  fconst2g  5700  fconstfvm  5703  resfunexg  5706  eufnfv  5715  foco2  5722  fniunfv  5730  fcofo  5752  fliftel  5761  fliftfun  5764  fliftfuns  5766  riota5f  5822  f1ocnvd  6040  suppssov1  6047  offval2  6065  ofrfval2  6066  offveqb  6069  caofref  6071  caofinvl  6072  opabex3d  6089  oprssdmm  6139  f1od2  6203  disjxp1  6204  tfrlem1  6276  tfrlemisucaccv  6293  tfrlemiubacc  6298  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemubacc  6314  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemubacc  6327  tfrcllemaccex  6329  tfrcllemres  6330  tfrcl  6332  rdgon  6354  freccllem  6370  frecfcllem  6372  omcl  6429  oeicl  6430  qliftfuns  6585  ixpeq2dva  6679  xpf1o  6810  mapxpen  6814  isinfinf  6863  fimax2gtrilemstep  6866  undifdcss  6888  eqsuptid  6962  eqinftid  6986  difinfsnlem  7064  difinfsn  7065  ctmlemr  7073  ctm  7074  ctssdclemn0  7075  ctssdccl  7076  enumctlemm  7079  nnnninf  7090  nnnninfeq  7092  enomnilem  7102  ismkvnex  7119  enmkvlem  7125  enwomnilem  7133  acfun  7163  exmidaclem  7164  exmidontriimlem4  7180  exmidontriim  7181  pw1on  7182  ccfunen  7205  cc2lem  7207  cc3  7209  genprndl  7462  genprndu  7463  nqprloc  7486  ltexprlemrnd  7546  ltexprlemdisj  7547  lteupri  7558  recexprlemrnd  7570  recexprlemdisj  7571  caucvgprlemlim  7622  caucvgprprlemlim  7652  suplocexprlemml  7657  suplocexprlemrl  7658  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  caucvgsrlembound  7735  caucvgsrlemgt1  7736  caucvgsrlemoffgt1  7740  caucvgsr  7743  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  elrealeu  7770  axcaucvglemcau  7839  axcaucvglemres  7840  axpre-suploclemres  7842  negeu  8089  eqord1  8381  eqord2  8382  creur  8854  creui  8855  suprzclex  9289  supinfneg  9533  infsupneg  9534  infregelbex  9536  indstr2  9547  iooidg  9845  iccsupr  9902  icoshftf1o  9927  fznlem  9976  exfzdc  10175  exbtwnzlemstep  10183  exbtwnzlemex  10185  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgtcl  10347  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgg  10351  frecuzrdgfunlem  10354  frecuzrdgsuctlem  10358  iseqovex  10391  seq3val  10393  seqvalcd  10394  seq3-1  10395  seqf  10396  seq3p1  10397  seqovcd  10398  seqp1cd  10401  seq3clss  10402  seq3fveq2  10404  seq3fveq  10406  seq3feq  10407  seq3shft2  10408  monoord  10411  monoord2  10412  ser3mono  10413  seq3split  10414  seq3caopr3  10416  seq3caopr2  10417  iseqf1olemqk  10429  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  iseqf1olemfvp  10432  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1oleml  10438  seq3f1o  10439  seq3id3  10442  seq3id  10443  seq3id2  10444  seq3homo  10445  seq3z  10446  ser3ge0  10452  nn0ltexp2  10623  bccl  10680  hashinfuni  10690  hashennnuni  10692  shftf  10772  seq3shft  10780  caucvgrelemcau  10922  cvg1nlemcau  10926  cvg1nlemres  10927  resqrexlemcvg  10961  resqrexlemglsq  10964  resqrexlemga  10965  maxabslemval  11150  negfi  11169  minmax  11171  xrmaxiflemval  11191  xrminmax  11206  climconst  11231  2clim  11242  climcn1  11249  climcn2  11250  reccn2ap  11254  cn1lem  11255  climsqz  11276  climsqz2  11277  climcau  11288  climrecvg1n  11289  serf0  11293  sumeq2dv  11309  sumrbdclem  11318  fsum3cvg  11319  summodclem3  11321  summodclem2a  11322  zsumdc  11325  isum  11326  fsumgcl  11327  fsum3  11328  fsumf1o  11331  isumss  11332  fisumss  11333  isumss2  11334  fsum3cvg2  11335  fsumsersdc  11336  fsum3ser  11338  fsumcl2lem  11339  fsumadd  11347  fsumsplit  11348  fsumm1  11357  fsum1p  11359  isumclim3  11364  isummulc2  11367  sumsplitdc  11373  fsum2dlemstep  11375  fisumcom2  11379  fsumshftm  11386  fsummulc2  11389  fsumge1  11402  fsum00  11403  fsumabs  11406  telfsumo  11407  telfsumo2  11408  fsumparts  11411  fsumrelem  11412  fsumiun  11418  hashiun  11419  hash2iun  11420  binomlem  11424  isumshft  11431  isum1p  11433  isumnn0nn  11434  isumrpcl  11435  isumlessdc  11437  divcnv  11438  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemseq  11467  cvgratnnlemabsle  11468  cvgratnnlemfm  11470  cvgratnnlemrate  11471  cvgratnn  11472  cvgratz  11473  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  clim2prod  11480  prodeq2dv  11507  prodrbdclem  11512  fproddccvg  11513  prodmodclem3  11516  prodmodclem2a  11517  zproddc  11520  iprodap  11521  fprodseq  11524  fprodf1o  11529  prodssdc  11530  fprodssdc  11531  fprodmul  11532  fprodsplit  11538  fprodm1  11539  fprod1p  11540  fprodm1s  11542  fprodp1s  11543  fprodunsn  11545  fprodcl2lem  11546  fprodabs  11557  fprodeq0  11558  fprodap0  11562  fprod2dlemstep  11563  fprodcom2fi  11567  fprodrec  11570  fprodmodd  11582  efcvgfsum  11608  dvdsssfz1  11790  zsupcllemstep  11878  infssuzex  11882  suprzubdc  11885  zsupssdc  11887  dvdsbnd  11889  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlemle  11941  bezoutlemsup  11942  dfgcd3  11943  dfgcd2  11947  nnwodc  11969  uzwodc  11970  nnwosdc  11972  coprmgcdb  12020  prmdc  12062  isprm5  12074  isprm6  12079  phivalfi  12144  phibndlem  12148  dfphi2  12152  hashdvds  12153  phiprmpw  12154  phimullem  12157  eulerthlemfi  12160  hashgcdeq  12171  phisum  12172  reumodprminv  12185  pclemdc  12220  pc2dvds  12261  pcz  12263  pcprmpw2  12264  pcmptdvds  12275  pcprod  12276  pcfac  12280  qexpz  12282  prmpwdvds  12285  pockthg  12287  infpnlem2  12290  1arithlem4  12296  1arith  12297  ennnfonelemex  12347  ennnfonelemfun  12350  ennnfonelemf1  12351  ennnfonelemnn0  12355  ennnfonelemim  12357  exmidunben  12359  ctinfomlemom  12360  ctinfom  12361  ctinf  12363  ctiunctlemudc  12370  ctiunctlemf  12371  ctiunctlemfo  12372  omctfn  12376  ssnnctlemct  12379  nninfdclemcl  12381  nninfdclemp1  12383  ismgmid2  12611  mgmidsssn0  12615  grprinvlem  12616  grprinvd  12617  fiinbas  12687  tgclb  12705  restbasg  12808  iscnp4  12858  cnco  12861  cnptopco  12862  cnss1  12866  cnss2  12867  cncnpi  12868  cncnp  12870  cnconst2  12873  cnrest  12875  cnptopresti  12878  cnpdis  12882  lmtopcnp  12890  txbasval  12907  tx1cn  12909  tx2cn  12910  txcnp  12911  upxp  12912  txdis1cn  12918  cnmpt11  12923  psmet0  12967  psmettri2  12968  psmetxrge0  12972  psmetres2  12973  ismeti  12986  xmetpsmet  13009  blsscls2  13133  comet  13139  xmettx  13150  tgioo  13186  tgqioo  13187  fsumcncntop  13196  elcncf1di  13206  cdivcncfap  13227  mulcncflem  13230  mulcncf  13231  cnopnap  13234  dedekindeulemuub  13235  dedekindeulemlu  13239  suplociccreex  13242  suplociccex  13243  dedekindicclemuub  13244  dedekindicclemlu  13248  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemdisj  13258  ivthinclemloc  13259  ivthinc  13261  ivthdec  13262  cnplimclemr  13278  limccnp2cntop  13286  limccoap  13287  dvcn  13304  dvfre  13314  dvrecap  13317  dvmptclx  13320  dvmptaddx  13321  dvmptmulx  13322  dveflem  13327  dvef  13328  sin0pilem1  13342  sin0pilem2  13343  lgsval2lem  13551  lgsdirnn0  13588  lgsdinn0  13589  2sqlem6  13596  2sqlem8  13599  2sqlem10  13601  fnmptd  13686  bj-charfun  13689  bj-charfundc  13690  bj-charfunr  13692  pw1nct  13883  nnsf  13885  nninfalllem1  13888  nninfall  13889  nninfself  13893  nninfsellemeq  13894  nninfsellemeqinf  13896  nninfsel  13897  isomninnlem  13909  trilpolemeq1  13919  trilpo  13922  apdiff  13927  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931  redcwlpo  13934  redc0  13936  reap0  13937  dceqnconst  13938  dcapnconst  13939  nconstwlpolem  13943  nconstwlpo  13944  neapmkv  13946