Theorem ralrimiva 2581

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
ralrimiva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Assertion

Ref	Expression
ralrimiva	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)
2	1	ex 115	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 2580	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2178  ∀wral 2486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  ralrimivvva  2591  rgen2  2594  rgen3  2595  nrexdv  2601  r19.29vva  2654  rabbidva  2765  ssrabdv  3281  ss2rabdv  3283  iuneq2dv  3963  iunssd  3988  disjeq2dv  4041  mpteq12dva  4142  triun  4172  issod  4385  frirrg  4416  frind  4418  peano2  4662  dmmptd  5427  fun11iun  5566  fniinfv  5662  eqfnfv  5702  eqfnfvd  5705  fnmptfvd  5709  dff3im  5750  dffo4  5753  fmptd  5759  ffnfv  5763  fmpt2d  5767  ffvresb  5768  funiun  5786  fconst2g  5824  fconstfvm  5827  resfunexg  5830  eufnfv  5840  foco2  5847  fniunfv  5856  fcofo  5878  fliftel  5887  fliftfun  5890  fliftfuns  5892  riota5f  5949  f1ocnvd  6173  suppssov1  6180  offval2  6199  ofrfval2  6200  offveqb  6203  offveq  6204  caofref  6208  caofinvl  6209  caofid0l  6210  caofid0r  6211  caofid1  6212  caofid2  6213  opabex3d  6231  uchoice  6248  oprssdmm  6282  f1od2  6346  disjxp1  6347  tfrlem1  6419  tfrlemisucaccv  6436  tfrlemiubacc  6441  tfr1onlemsucfn  6451  tfr1onlemsucaccv  6452  tfr1onlembxssdm  6454  tfr1onlembfn  6455  tfr1onlemubacc  6457  tfr1onlemaccex  6459  tfr1onlemres  6460  tfrcllemsucfn  6464  tfrcllemsucaccv  6465  tfrcllembxssdm  6467  tfrcllembfn  6468  tfrcllemubacc  6470  tfrcllemaccex  6472  tfrcllemres  6473  tfrcl  6475  rdgon  6497  freccllem  6513  frecfcllem  6515  omcl  6572  oeicl  6573  qliftfuns  6731  ixpeq2dva  6825  xpf1o  6968  mapxpen  6972  isinfinf  7022  fimax2gtrilemstep  7025  undifdcss  7048  opabfi  7063  eqsuptid  7127  eqinftid  7151  difinfsnlem  7229  difinfsn  7230  ctmlemr  7238  ctm  7239  ctssdclemn0  7240  ctssdccl  7241  enumctlemm  7244  nninfninc  7253  nnnninf  7256  nnnninfeq  7258  enomnilem  7268  ismkvnex  7285  enmkvlem  7291  enwomnilem  7299  nninfwlporlemd  7302  nninfwlpoimlemg  7305  nninfwlpoimlemginf  7306  nninfwlpoim  7309  nninfinfwlpo  7310  finacn  7349  acfun  7352  exmidaclem  7353  exmidontriimlem4  7369  exmidontriim  7370  pw1on  7374  ccfunen  7413  cc2lem  7415  cc3  7417  acnccim  7421  genprndl  7671  genprndu  7672  nqprloc  7695  ltexprlemrnd  7755  ltexprlemdisj  7756  lteupri  7767  recexprlemrnd  7779  recexprlemdisj  7780  caucvgprlemlim  7831  caucvgprprlemlim  7861  suplocexprlemml  7866  suplocexprlemrl  7867  suplocexprlemmu  7868  suplocexprlemru  7869  suplocexprlemdisj  7870  suplocexprlemloc  7871  suplocexprlemub  7873  caucvgsrlembound  7944  caucvgsrlemgt1  7945  caucvgsrlemoffgt1  7949  caucvgsr  7952  suplocsrlemb  7956  suplocsrlempr  7957  suplocsrlem  7958  elrealeu  7979  axcaucvglemcau  8048  axcaucvglemres  8049  axpre-suploclemres  8051  negeu  8300  eqord1  8593  eqord2  8594  creur  9069  creui  9070  suprzclex  9508  supinfneg  9753  infsupneg  9754  infregelbex  9756  indstr2  9767  iooidg  10068  iccsupr  10125  icoshftf1o  10150  fznlem  10200  exfzdc  10408  zsupcllemstep  10411  infssuzex  10415  suprzubdc  10418  zsupssdc  10420  exbtwnzlemstep  10429  exbtwnzlemex  10431  frec2uzrdg  10593  frecuzrdgrcl  10594  frecuzrdgtcl  10596  frecuzrdgsuc  10598  frecuzrdgrclt  10599  frecuzrdgg  10600  frecuzrdgfunlem  10603  frecuzrdgsuctlem  10607  nninfinf  10627  iseqovex  10642  seq3val  10644  seqvalcd  10645  seq3-1  10646  seqf  10648  seq3p1  10649  seqovcd  10651  seqp1cd  10654  seq3clss  10655  seq3fveq2  10659  seqfveq2g  10661  seqfveqg  10662  seq3fveq  10663  seq3feq  10664  seq3shft2  10665  seqshft2g  10666  monoord  10669  monoord2  10670  ser3mono  10671  seq3split  10672  seqsplitg  10673  seq3caopr3  10675  seqcaopr3g  10676  seq3caopr2  10677  seqcaopr2g  10678  iseqf1olemqk  10691  iseqf1olemjpcl  10692  iseqf1olemqpcl  10693  iseqf1olemfvp  10694  seq3f1olemqsumkj  10695  seq3f1olemqsumk  10696  seq3f1olemqsum  10697  seq3f1oleml  10700  seq3f1o  10701  seqf1og  10705  seq3id3  10708  seq3id  10709  seq3id2  10710  seq3homo  10711  seq3z  10712  seqhomog  10714  seqfeq4g  10715  ser3ge0  10720  nn0ltexp2  10893  bccl  10951  hashinfuni  10961  hashennnuni  10963  wrdexg  11044  ccatlen  11091  ccatvalfn  11097  ccatrn  11105  swrdlen  11145  swrdwrdsymbg  11157  swrdswrd  11198  wrdind  11215  reuccatpfxs1  11240  shftf  11302  seq3shft  11310  caucvgrelemcau  11452  cvg1nlemcau  11456  cvg1nlemres  11457  resqrexlemcvg  11491  resqrexlemglsq  11494  resqrexlemga  11495  maxabslemval  11680  negfi  11700  minmax  11702  xrmaxiflemval  11722  xrminmax  11737  climconst  11762  2clim  11773  climcn1  11780  climcn2  11781  reccn2ap  11785  cn1lem  11786  climsqz  11807  climsqz2  11808  climcau  11819  climrecvg1n  11820  serf0  11824  sumeq2dv  11840  sumrbdclem  11849  fsum3cvg  11850  summodclem3  11852  summodclem2a  11853  zsumdc  11856  isum  11857  fsumgcl  11858  fsum3  11859  fsumf1o  11862  isumss  11863  fisumss  11864  isumss2  11865  fsum3cvg2  11866  fsumsersdc  11867  fsum3ser  11869  fsumcl2lem  11870  fsumadd  11878  fsumsplit  11879  fsumm1  11888  fsum1p  11890  isumclim3  11895  isummulc2  11898  sumsplitdc  11904  fsum2dlemstep  11906  fisumcom2  11910  fsumshftm  11917  fsummulc2  11920  fsumge1  11933  fsum00  11934  fsumabs  11937  telfsumo  11938  telfsumo2  11939  fsumparts  11942  fsumrelem  11943  fsumiun  11949  hashiun  11950  hash2iun  11951  binomlem  11955  isumshft  11962  isum1p  11964  isumnn0nn  11965  isumrpcl  11966  isumlessdc  11968  divcnv  11969  cvgratnnlemnexp  11996  cvgratnnlemmn  11997  cvgratnnlemseq  11998  cvgratnnlemabsle  11999  cvgratnnlemfm  12001  cvgratnnlemrate  12002  cvgratnn  12003  cvgratz  12004  mertenslemi1  12007  mertenslem2  12008  mertensabs  12009  clim2prod  12011  prodeq2dv  12038  prodrbdclem  12043  fproddccvg  12044  prodmodclem3  12047  prodmodclem2a  12048  zproddc  12051  iprodap  12052  fprodseq  12055  fprodf1o  12060  prodssdc  12061  fprodssdc  12062  fprodmul  12063  fprodsplit  12069  fprodm1  12070  fprod1p  12071  fprodm1s  12073  fprodp1s  12074  fprodunsn  12076  fprodcl2lem  12077  fprodabs  12088  fprodeq0  12089  fprodap0  12093  fprod2dlemstep  12094  fprodcom2fi  12098  fprodrec  12101  fprodmodd  12113  efcvgfsum  12139  dvdsssfz1  12324  bitsfi  12429  bitsinv1  12434  dvdsbnd  12438  bezoutlemstep  12479  bezoutlemmain  12480  bezoutlemle  12490  bezoutlemsup  12491  dfgcd3  12492  dfgcd2  12496  nnwodc  12518  uzwodc  12519  nnwosdc  12521  nninfctlemfo  12522  coprmgcdb  12571  prmdc  12613  isprm5  12625  isprm6  12630  phivalfi  12695  phibndlem  12699  dfphi2  12703  hashdvds  12704  phiprmpw  12705  phimullem  12708  eulerthlemfi  12711  dvdsfi  12722  hashgcdeq  12723  phisum  12724  reumodprminv  12737  pclemdc  12772  pc2dvds  12814  pcz  12816  pcprmpw2  12817  pcmptdvds  12829  pcprod  12830  pcfac  12834  qexpz  12836  prmpwdvds  12839  pockthg  12841  infpnlem2  12844  1arithlem4  12850  1arith  12851  4sqlemafi  12879  4sqlemffi  12880  4sqleminfi  12881  ennnfonelemex  12946  ennnfonelemfun  12949  ennnfonelemf1  12950  ennnfonelemnn0  12954  ennnfonelemim  12956  exmidunben  12958  ctinfomlemom  12959  ctinfom  12960  ctinf  12962  ctiunctlemudc  12969  ctiunctlemf  12970  ctiunctlemfo  12971  omctfn  12975  ssnnctlemct  12978  nninfdclemcl  12980  nninfdclemp1  12982  pwsbas  13285  imasival  13299  ismgmid2  13373  mgmidsssn0  13377  grpinvalem  13378  grpinva  13379  gsumress  13388  issgrpd  13405  prdsplusgsgrpcl  13407  sgrpidmndm  13413  ismndd  13430  mndpfo  13431  prdsplusgcl  13439  prdsidlem  13440  mhmima  13484  mhmeql  13485  gsumvallem2  13486  isgrpd2e  13513  dfgrp2  13520  grpidd2  13534  isgrpinv  13547  grplrinv  13550  grpidinv  13552  dfgrp3me  13593  prdsinvlem  13601  mhmmnd  13613  ghmgrp  13615  mulgsubcl  13633  issubg2m  13686  issubgrpd2  13687  grpissubg  13691  subgintm  13695  nmzsubg  13707  ssnmz  13708  ghmrn  13754  ghmeql  13764  ghmf1  13770  conjnmz  13776  conjnmzb  13777  rinvmod  13806  srgrz  13907  srglz  13908  srgisid  13909  ringsrg  13970  rhmdvdsr  14098  rhmopp  14099  subrngintm  14135  subrg1  14154  subrgugrp  14163  subrgintm  14166  unitrrg  14190  aprap  14209  islmodd  14216  lssuni  14286  lsssubg  14300  lssintclm  14307  dflidl2rng  14404  lidlsubg  14409  cnsubglem  14502  gsumfzfsumlemm  14510  znf1o  14574  znidomb  14581  psrbagfi  14596  psr1clfi  14611  mplsubgfilemm  14621  mplsubgfilemcl  14622  mplsubgfi  14624  fiinbas  14682  tgclb  14698  restbasg  14801  iscnp4  14851  cnco  14854  cnptopco  14855  cnss1  14859  cnss2  14860  cncnpi  14861  cncnp  14863  cnconst2  14866  cnrest  14868  cnptopresti  14871  cnpdis  14875  lmtopcnp  14883  txbasval  14900  tx1cn  14902  tx2cn  14903  txcnp  14904  upxp  14905  txdis1cn  14911  cnmpt11  14916  psmet0  14960  psmettri2  14961  psmetxrge0  14965  psmetres2  14966  ismeti  14979  xmetpsmet  15002  blsscls2  15126  comet  15132  xmettx  15143  tgioo  15187  tgqioo  15188  fsumcncntop  15200  elcncf1di  15212  cdivcncfap  15237  mulcncflem  15240  mulcncf  15241  cnopnap  15244  divcncfap  15247  dedekindeulemuub  15250  dedekindeulemlu  15254  suplociccreex  15257  suplociccex  15258  dedekindicclemuub  15259  dedekindicclemlu  15263  ivthinclemlopn  15269  ivthinclemlr  15270  ivthinclemuopn  15271  ivthinclemur  15272  ivthinclemdisj  15273  ivthinclemloc  15274  ivthinc  15276  ivthdec  15277  dich0  15285  ivthdich  15286  cnplimclemr  15302  limccnp2cntop  15310  limccoap  15311  dvcn  15333  dvfre  15343  dvrecap  15346  dvmptclx  15351  dvmptaddx  15352  dvmptmulx  15353  dveflem  15359  dvef  15360  ply1termlem  15375  plyaddlem1  15380  plymullem1  15381  plycoeid3  15390  plycj  15394  plyreres  15397  dvply1  15398  sin0pilem1  15414  sin0pilem2  15415  mpodvdsmulf1o  15623  mersenne  15630  perfectlem2  15633  lgsval2lem  15648  lgsdirnn0  15685  lgsdinn0  15686  gausslemma2dlem1f1o  15698  gausslemma2dlem2  15700  gausslemma2dlem3  15701  lgsquadlemofi  15714  lgsquadlem1  15715  lgsquadlem2  15716  2lgslem1a1  15724  2sqlem6  15758  2sqlem8  15761  2sqlem10  15763  usgruspgrben  15941  fnmptd  16048  bj-charfun  16050  bj-charfundc  16051  bj-charfunr  16053  2omap  16240  pw1nct  16250  nnsf  16252  nninfalllem1  16255  nninfall  16256  nninfself  16260  nninfsellemeq  16261  nninfsellemeqinf  16263  nninfsel  16264  nnnninfex  16269  nninfnfiinf  16270  isomninnlem  16279  trilpolemeq1  16289  trilpo  16292  apdiff  16297  iswomninnlem  16298  iswomni0  16300  ismkvnnlem  16301  redcwlpo  16304  redc0  16306  reap0  16307  dceqnconst  16309  dcapnconst  16310  nconstwlpolem  16314  nconstwlpo  16315  neapmkv  16317  ltlenmkv  16319