Theorem ralrimiva 2508

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

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

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  ralrimivvva  2518  rgen2  2521  rgen3  2522  nrexdv  2528  r19.29vva  2580  rabbidva  2677  ssrabdv  3181  ss2rabdv  3183  iuneq2dv  3842  disjeq2dv  3919  mpteq12dva  4017  triun  4047  issod  4249  frirrg  4280  frind  4282  peano2  4517  dmmptd  5261  fun11iun  5396  fniinfv  5487  eqfnfv  5526  eqfnfvd  5529  dff3im  5573  dffo4  5576  fmptd  5582  ffnfv  5586  fmpt2d  5590  ffvresb  5591  fconst2g  5643  fconstfvm  5646  resfunexg  5649  eufnfv  5656  foco2  5663  fniunfv  5671  fcofo  5693  fliftel  5702  fliftfun  5705  fliftfuns  5707  riota5f  5762  grprinvlem  5973  grprinvd  5974  f1ocnvd  5980  suppssov1  5987  offval2  6005  ofrfval2  6006  offveqb  6009  caofref  6011  caofinvl  6012  opabex3d  6027  oprssdmm  6077  f1od2  6140  disjxp1  6141  tfrlem1  6213  tfrlemisucaccv  6230  tfrlemiubacc  6235  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemubacc  6251  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemubacc  6264  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  rdgon  6291  freccllem  6307  frecfcllem  6309  omcl  6365  oeicl  6366  qliftfuns  6521  ixpeq2dva  6615  xpf1o  6746  mapxpen  6750  isinfinf  6799  fimax2gtrilemstep  6802  undifdcss  6819  eqsuptid  6892  eqinftid  6916  difinfsnlem  6992  difinfsn  6993  ctmlemr  7001  ctm  7002  ctssdclemn0  7003  ctssdccl  7004  enumctlemm  7007  enomnilem  7018  nnnninf  7031  ismkvnex  7037  enmkvlem  7043  enwomnilem  7050  acfun  7080  exmidaclem  7081  ccfunen  7096  cc2lem  7098  cc3  7100  genprndl  7353  genprndu  7354  nqprloc  7377  ltexprlemrnd  7437  ltexprlemdisj  7438  lteupri  7449  recexprlemrnd  7461  recexprlemdisj  7462  caucvgprlemlim  7513  caucvgprprlemlim  7543  suplocexprlemml  7548  suplocexprlemrl  7549  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  caucvgsrlembound  7626  caucvgsrlemgt1  7627  caucvgsrlemoffgt1  7631  caucvgsr  7634  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  elrealeu  7661  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  negeu  7977  eqord1  8269  eqord2  8270  creur  8741  creui  8742  suprzclex  9173  supinfneg  9417  infsupneg  9418  indstr2  9430  iooidg  9722  iccsupr  9779  icoshftf1o  9804  fznlem  9852  exfzdc  10048  exbtwnzlemstep  10056  exbtwnzlemex  10058  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgtcl  10216  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgfunlem  10223  frecuzrdgsuctlem  10227  iseqovex  10260  seq3val  10262  seqvalcd  10263  seq3-1  10264  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  seq3clss  10271  seq3fveq2  10273  seq3fveq  10275  seq3feq  10276  seq3shft2  10277  monoord  10280  monoord2  10281  ser3mono  10282  seq3split  10283  seq3caopr3  10285  seq3caopr2  10286  iseqf1olemqk  10298  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1oleml  10307  seq3f1o  10308  seq3id3  10311  seq3id  10312  seq3id2  10313  seq3homo  10314  seq3z  10315  ser3ge0  10321  bccl  10545  hashinfuni  10555  hashennnuni  10557  shftf  10634  seq3shft  10642  caucvgrelemcau  10784  cvg1nlemcau  10788  cvg1nlemres  10789  resqrexlemcvg  10823  resqrexlemglsq  10826  resqrexlemga  10827  maxabslemval  11012  negfi  11031  minmax  11033  xrmaxiflemval  11051  xrminmax  11066  climconst  11091  2clim  11102  climcn1  11109  climcn2  11110  reccn2ap  11114  cn1lem  11115  climsqz  11136  climsqz2  11137  climcau  11148  climrecvg1n  11149  serf0  11153  sumeq2dv  11169  sumrbdclem  11178  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  zsumdc  11185  isum  11186  fsumgcl  11187  fsum3  11188  fsumf1o  11191  isumss  11192  fisumss  11193  isumss2  11194  fsum3cvg2  11195  fsumsersdc  11196  fsum3ser  11198  fsumcl2lem  11199  fsumadd  11207  fsumsplit  11208  fsumm1  11217  fsum1p  11219  isumclim3  11224  isummulc2  11227  sumsplitdc  11233  fsum2dlemstep  11235  fisumcom2  11239  fsumshftm  11246  fsummulc2  11249  fsumge1  11262  fsum00  11263  fsumabs  11266  telfsumo  11267  telfsumo2  11268  fsumparts  11271  fsumrelem  11272  fsumiun  11278  hashiun  11279  hash2iun  11280  binomlem  11284  isumshft  11291  isum1p  11293  isumnn0nn  11294  isumrpcl  11295  isumlessdc  11297  divcnv  11298  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemseq  11327  cvgratnnlemabsle  11328  cvgratnnlemfm  11330  cvgratnnlemrate  11331  cvgratnn  11332  cvgratz  11333  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  clim2prod  11340  prodeq2dv  11367  prodrbdclem  11372  fproddccvg  11373  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  iprodap  11381  fprodseq  11384  efcvgfsum  11410  dvdsssfz1  11586  zsupcllemstep  11674  infssuzex  11678  dvdsbnd  11681  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemle  11732  bezoutlemsup  11733  dfgcd3  11734  dfgcd2  11738  coprmgcdb  11805  isprm6  11861  phivalfi  11924  phibndlem  11928  dfphi2  11932  hashdvds  11933  phiprmpw  11934  phimullem  11937  hashgcdeq  11940  ennnfonelemex  11963  ennnfonelemfun  11966  ennnfonelemf1  11967  ennnfonelemnn0  11971  ennnfonelemim  11973  exmidunben  11975  ctinfomlemom  11976  ctinfom  11977  ctinf  11979  ctiunctlemudc  11986  ctiunctlemf  11987  ctiunctlemfo  11988  omctfn  11992  fiinbas  12255  tgclb  12273  restbasg  12376  iscnp4  12426  cnco  12429  cnptopco  12430  cnss1  12434  cnss2  12435  cncnpi  12436  cncnp  12438  cnconst2  12441  cnrest  12443  cnptopresti  12446  cnpdis  12450  lmtopcnp  12458  txbasval  12475  tx1cn  12477  tx2cn  12478  txcnp  12479  upxp  12480  txdis1cn  12486  cnmpt11  12491  psmet0  12535  psmettri2  12536  psmetxrge0  12540  psmetres2  12541  ismeti  12554  xmetpsmet  12577  blsscls2  12701  comet  12707  xmettx  12718  tgioo  12754  tgqioo  12755  fsumcncntop  12764  elcncf1di  12774  cdivcncfap  12795  mulcncflem  12798  mulcncf  12799  cnopnap  12802  dedekindeulemuub  12803  dedekindeulemlu  12807  suplociccreex  12810  suplociccex  12811  dedekindicclemuub  12812  dedekindicclemlu  12816  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemdisj  12826  ivthinclemloc  12827  ivthinc  12829  ivthdec  12830  cnplimclemr  12846  limccnp2cntop  12854  limccoap  12855  dvcn  12872  dvfre  12882  dvrecap  12885  dvmptclx  12888  dvmptaddx  12889  dvmptmulx  12890  dveflem  12895  dvef  12896  sin0pilem1  12910  sin0pilem2  12911  pw1nct  13371  nnsf  13374  nninfalllemn  13377  nninfalllem1  13378  nninfall  13379  nninfself  13384  nninfsellemeq  13385  nninfsellemeqinf  13387  nninfsel  13388  isomninnlem  13400  trilpolemeq1  13408  trilpo  13411  apdiff  13416  iswomninnlem  13417  ismkvnnlem  13419  redcwlpo  13422  dceqnconst  13423  neapmkv  13425