Theorem ralrimiva 2505

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

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  ralrimivvva  2515  rgen2  2518  rgen3  2519  nrexdv  2525  r19.29vva  2577  rabbidva  2674  ssrabdv  3176  ss2rabdv  3178  iuneq2dv  3834  disjeq2dv  3911  mpteq12dva  4009  triun  4039  issod  4241  frirrg  4272  frind  4274  peano2  4509  dmmptd  5253  fun11iun  5388  fniinfv  5479  eqfnfv  5518  eqfnfvd  5521  dff3im  5565  dffo4  5568  fmptd  5574  ffnfv  5578  fmpt2d  5582  ffvresb  5583  fconst2g  5635  fconstfvm  5638  resfunexg  5641  eufnfv  5648  foco2  5655  fniunfv  5663  fcofo  5685  fliftel  5694  fliftfun  5697  fliftfuns  5699  riota5f  5754  grprinvlem  5965  grprinvd  5966  f1ocnvd  5972  suppssov1  5979  offval2  5997  ofrfval2  5998  offveqb  6001  caofref  6003  caofinvl  6004  opabex3d  6019  oprssdmm  6069  f1od2  6132  disjxp1  6133  tfrlem1  6205  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemubacc  6243  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemubacc  6256  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  rdgon  6283  freccllem  6299  frecfcllem  6301  omcl  6357  oeicl  6358  qliftfuns  6513  ixpeq2dva  6607  xpf1o  6738  mapxpen  6742  isinfinf  6791  fimax2gtrilemstep  6794  undifdcss  6811  eqsuptid  6884  eqinftid  6908  difinfsnlem  6984  difinfsn  6985  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  enumctlemm  6999  enomnilem  7010  nnnninf  7023  ismkvnex  7029  acfun  7063  exmidaclem  7064  ccfunen  7079  genprndl  7329  genprndu  7330  nqprloc  7353  ltexprlemrnd  7413  ltexprlemdisj  7414  lteupri  7425  recexprlemrnd  7437  recexprlemdisj  7438  caucvgprlemlim  7489  caucvgprprlemlim  7519  suplocexprlemml  7524  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  caucvgsrlembound  7602  caucvgsrlemgt1  7603  caucvgsrlemoffgt1  7607  caucvgsr  7610  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  elrealeu  7637  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  negeu  7953  eqord1  8245  eqord2  8246  creur  8717  creui  8718  suprzclex  9149  supinfneg  9390  infsupneg  9391  indstr2  9403  iooidg  9692  iccsupr  9749  icoshftf1o  9774  fznlem  9821  exfzdc  10017  exbtwnzlemstep  10025  exbtwnzlemex  10027  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgtcl  10185  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgfunlem  10192  frecuzrdgsuctlem  10196  iseqovex  10229  seq3val  10231  seqvalcd  10232  seq3-1  10233  seqf  10234  seq3p1  10235  seqovcd  10236  seqp1cd  10239  seq3clss  10240  seq3fveq2  10242  seq3fveq  10244  seq3feq  10245  seq3shft2  10246  monoord  10249  monoord2  10250  ser3mono  10251  seq3split  10252  seq3caopr3  10254  seq3caopr2  10255  iseqf1olemqk  10267  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  iseqf1olemfvp  10270  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1oleml  10276  seq3f1o  10277  seq3id3  10280  seq3id  10281  seq3id2  10282  seq3homo  10283  seq3z  10284  ser3ge0  10290  bccl  10513  hashinfuni  10523  hashennnuni  10525  shftf  10602  seq3shft  10610  caucvgrelemcau  10752  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemcvg  10791  resqrexlemglsq  10794  resqrexlemga  10795  maxabslemval  10980  negfi  10999  minmax  11001  xrmaxiflemval  11019  xrminmax  11034  climconst  11059  2clim  11070  climcn1  11077  climcn2  11078  reccn2ap  11082  cn1lem  11083  climsqz  11104  climsqz2  11105  climcau  11116  climrecvg1n  11117  serf0  11121  sumeq2dv  11137  sumrbdclem  11146  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  zsumdc  11153  isum  11154  fsumgcl  11155  fsum3  11156  fsumf1o  11159  isumss  11160  fisumss  11161  isumss2  11162  fsum3cvg2  11163  fsumsersdc  11164  fsum3ser  11166  fsumcl2lem  11167  fsumadd  11175  fsumsplit  11176  fsumm1  11185  fsum1p  11187  isumclim3  11192  isummulc2  11195  sumsplitdc  11201  fsum2dlemstep  11203  fisumcom2  11207  fsumshftm  11214  fsummulc2  11217  fsumge1  11230  fsum00  11231  fsumabs  11234  telfsumo  11235  telfsumo2  11236  fsumparts  11239  fsumrelem  11240  fsumiun  11246  hashiun  11247  hash2iun  11248  binomlem  11252  isumshft  11259  isum1p  11261  isumnn0nn  11262  isumrpcl  11263  isumlessdc  11265  divcnv  11266  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemseq  11295  cvgratnnlemabsle  11296  cvgratnnlemfm  11298  cvgratnnlemrate  11299  cvgratnn  11300  cvgratz  11301  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  clim2prod  11308  prodeq2dv  11335  prodrbdclem  11340  fproddccvg  11341  prodmodclem3  11344  prodmodclem2a  11345  efcvgfsum  11373  dvdsssfz1  11550  zsupcllemstep  11638  infssuzex  11642  dvdsbnd  11645  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemle  11696  bezoutlemsup  11697  dfgcd3  11698  dfgcd2  11702  coprmgcdb  11769  isprm6  11825  phivalfi  11888  phibndlem  11892  dfphi2  11896  hashdvds  11897  phiprmpw  11898  phimullem  11901  hashgcdeq  11904  ennnfonelemex  11927  ennnfonelemfun  11930  ennnfonelemf1  11931  ennnfonelemnn0  11935  ennnfonelemim  11937  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  ctinf  11943  ctiunctlemudc  11950  ctiunctlemf  11951  ctiunctlemfo  11952  fiinbas  12216  tgclb  12234  restbasg  12337  iscnp4  12387  cnco  12390  cnptopco  12391  cnss1  12395  cnss2  12396  cncnpi  12397  cncnp  12399  cnconst2  12402  cnrest  12404  cnptopresti  12407  cnpdis  12411  lmtopcnp  12419  txbasval  12436  tx1cn  12438  tx2cn  12439  txcnp  12440  upxp  12441  txdis1cn  12447  cnmpt11  12452  psmet0  12496  psmettri2  12497  psmetxrge0  12501  psmetres2  12502  ismeti  12515  xmetpsmet  12538  blsscls2  12662  comet  12668  xmettx  12679  tgioo  12715  tgqioo  12716  fsumcncntop  12725  elcncf1di  12735  cdivcncfap  12756  mulcncflem  12759  mulcncf  12760  cnopnap  12763  dedekindeulemuub  12764  dedekindeulemlu  12768  suplociccreex  12771  suplociccex  12772  dedekindicclemuub  12773  dedekindicclemlu  12777  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemdisj  12787  ivthinclemloc  12788  ivthinc  12790  ivthdec  12791  cnplimclemr  12807  limccnp2cntop  12815  limccoap  12816  dvcn  12833  dvfre  12843  dvrecap  12846  dvmptclx  12849  dvmptaddx  12850  dvmptmulx  12851  dveflem  12855  dvef  12856  sin0pilem1  12862  sin0pilem2  12863  nnsf  13199  nninfalllemn  13202  nninfalllem1  13203  nninfall  13204  nninfself  13209  nninfsellemeq  13210  nninfsellemeqinf  13212  nninfsel  13213  isomninnlem  13225  trilpolemeq1  13233  trilpo  13236