Theorem ralrimiva 2503

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

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

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 2419

This theorem is referenced by:  ralrimivvva  2513  rgen2  2516  rgen3  2517  nrexdv  2523  r19.29vva  2575  rabbidva  2669  ssrabdv  3171  ss2rabdv  3173  iuneq2dv  3829  disjeq2dv  3906  mpteq12dva  4004  triun  4034  issod  4236  frirrg  4267  frind  4269  peano2  4504  dmmptd  5248  fun11iun  5381  fniinfv  5472  eqfnfv  5511  eqfnfvd  5514  dff3im  5558  dffo4  5561  fmptd  5567  ffnfv  5571  fmpt2d  5575  ffvresb  5576  fconst2g  5628  fconstfvm  5631  resfunexg  5634  eufnfv  5641  foco2  5648  fniunfv  5656  fcofo  5678  fliftel  5687  fliftfun  5690  fliftfuns  5692  riota5f  5747  grprinvlem  5958  grprinvd  5959  f1ocnvd  5965  suppssov1  5972  offval2  5990  ofrfval2  5991  offveqb  5994  caofref  5996  caofinvl  5997  opabex3d  6012  oprssdmm  6062  f1od2  6125  disjxp1  6126  tfrlem1  6198  tfrlemisucaccv  6215  tfrlemiubacc  6220  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemubacc  6236  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemubacc  6249  tfrcllemaccex  6251  tfrcllemres  6252  tfrcl  6254  rdgon  6276  freccllem  6292  frecfcllem  6294  omcl  6350  oeicl  6351  qliftfuns  6506  ixpeq2dva  6600  xpf1o  6731  mapxpen  6735  isinfinf  6784  fimax2gtrilemstep  6787  undifdcss  6804  eqsuptid  6877  eqinftid  6901  difinfsnlem  6977  difinfsn  6978  ctmlemr  6986  ctm  6987  ctssdclemn0  6988  ctssdccl  6989  enumctlemm  6992  enomnilem  7003  nnnninf  7016  ismkvnex  7022  acfun  7056  exmidaclem  7057  ccfunen  7072  genprndl  7322  genprndu  7323  nqprloc  7346  ltexprlemrnd  7406  ltexprlemdisj  7407  lteupri  7418  recexprlemrnd  7430  recexprlemdisj  7431  caucvgprlemlim  7482  caucvgprprlemlim  7512  suplocexprlemml  7517  suplocexprlemrl  7518  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemub  7524  caucvgsrlembound  7595  caucvgsrlemgt1  7596  caucvgsrlemoffgt1  7600  caucvgsr  7603  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  elrealeu  7630  axcaucvglemcau  7699  axcaucvglemres  7700  axpre-suploclemres  7702  negeu  7946  eqord1  8238  eqord2  8239  creur  8710  creui  8711  suprzclex  9142  supinfneg  9383  infsupneg  9384  indstr2  9396  iooidg  9685  iccsupr  9742  icoshftf1o  9767  fznlem  9814  exfzdc  10010  exbtwnzlemstep  10018  exbtwnzlemex  10020  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgtcl  10178  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  frecuzrdgfunlem  10185  frecuzrdgsuctlem  10189  iseqovex  10222  seq3val  10224  seqvalcd  10225  seq3-1  10226  seqf  10227  seq3p1  10228  seqovcd  10229  seqp1cd  10232  seq3clss  10233  seq3fveq2  10235  seq3fveq  10237  seq3feq  10238  seq3shft2  10239  monoord  10242  monoord2  10243  ser3mono  10244  seq3split  10245  seq3caopr3  10247  seq3caopr2  10248  iseqf1olemqk  10260  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  iseqf1olemfvp  10263  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3f1oleml  10269  seq3f1o  10270  seq3id3  10273  seq3id  10274  seq3id2  10275  seq3homo  10276  seq3z  10277  ser3ge0  10283  bccl  10506  hashinfuni  10516  hashennnuni  10518  shftf  10595  seq3shft  10603  caucvgrelemcau  10745  cvg1nlemcau  10749  cvg1nlemres  10750  resqrexlemcvg  10784  resqrexlemglsq  10787  resqrexlemga  10788  maxabslemval  10973  negfi  10992  minmax  10994  xrmaxiflemval  11012  xrminmax  11027  climconst  11052  2clim  11063  climcn1  11070  climcn2  11071  reccn2ap  11075  cn1lem  11076  climsqz  11097  climsqz2  11098  climcau  11109  climrecvg1n  11110  serf0  11114  sumeq2dv  11130  sumrbdclem  11138  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  zsumdc  11146  isum  11147  fsumgcl  11148  fsum3  11149  fsumf1o  11152  isumss  11153  fisumss  11154  isumss2  11155  fsum3cvg2  11156  fsumsersdc  11157  fsum3ser  11159  fsumcl2lem  11160  fsumadd  11168  fsumsplit  11169  fsumm1  11178  fsum1p  11180  isumclim3  11185  isummulc2  11188  sumsplitdc  11194  fsum2dlemstep  11196  fisumcom2  11200  fsumshftm  11207  fsummulc2  11210  fsumge1  11223  fsum00  11224  fsumabs  11227  telfsumo  11228  telfsumo2  11229  fsumparts  11232  fsumrelem  11233  fsumiun  11239  hashiun  11240  hash2iun  11241  binomlem  11245  isumshft  11252  isum1p  11254  isumnn0nn  11255  isumrpcl  11256  isumlessdc  11258  divcnv  11259  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemseq  11288  cvgratnnlemabsle  11289  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratnn  11293  cvgratz  11294  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  clim2prod  11301  prodeq2dv  11328  prodrbdclem  11333  fproddccvg  11334  efcvgfsum  11362  dvdsssfz1  11539  zsupcllemstep  11627  infssuzex  11631  dvdsbnd  11634  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlemle  11685  bezoutlemsup  11686  dfgcd3  11687  dfgcd2  11691  coprmgcdb  11758  isprm6  11814  phivalfi  11877  phibndlem  11881  dfphi2  11885  hashdvds  11886  phiprmpw  11887  phimullem  11890  hashgcdeq  11893  ennnfonelemex  11916  ennnfonelemfun  11919  ennnfonelemf1  11920  ennnfonelemnn0  11924  ennnfonelemim  11926  exmidunben  11928  ctinfomlemom  11929  ctinfom  11930  ctinf  11932  ctiunctlemudc  11939  ctiunctlemf  11940  ctiunctlemfo  11941  fiinbas  12205  tgclb  12223  restbasg  12326  iscnp4  12376  cnco  12379  cnptopco  12380  cnss1  12384  cnss2  12385  cncnpi  12386  cncnp  12388  cnconst2  12391  cnrest  12393  cnptopresti  12396  cnpdis  12400  lmtopcnp  12408  txbasval  12425  tx1cn  12427  tx2cn  12428  txcnp  12429  upxp  12430  txdis1cn  12436  cnmpt11  12441  psmet0  12485  psmettri2  12486  psmetxrge0  12490  psmetres2  12491  ismeti  12504  xmetpsmet  12527  blsscls2  12651  comet  12657  xmettx  12668  tgioo  12704  tgqioo  12705  fsumcncntop  12714  elcncf1di  12724  cdivcncfap  12745  mulcncflem  12748  mulcncf  12749  cnopnap  12752  dedekindeulemuub  12753  dedekindeulemlu  12757  suplociccreex  12760  suplociccex  12761  dedekindicclemuub  12762  dedekindicclemlu  12766  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemdisj  12776  ivthinclemloc  12777  ivthinc  12779  ivthdec  12780  cnplimclemr  12796  limccnp2cntop  12804  limccoap  12805  dvcn  12822  dvfre  12832  dvrecap  12835  dvmptclx  12838  dvmptaddx  12839  dvmptmulx  12840  dveflem  12844  dvef  12845  sin0pilem1  12851  sin0pilem2  12852  nnsf  13188  nninfalllemn  13191  nninfalllem1  13192  nninfall  13193  nninfself  13198  nninfsellemeq  13199  nninfsellemeqinf  13201  nninfsel  13202  isomninnlem  13214  trilpolemeq1  13222  trilpo  13225