Theorem ralrimiva 2605

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 2604	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∀wral 2510

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralrimivvva  2615  rgen2  2618  rgen3  2619  nrexdv  2625  r19.29vva  2678  rabbidva  2790  ssrabdv  3306  ss2rabdv  3308  iuneq2dv  3991  iunssd  4016  disjeq2dv  4069  mpteq12dva  4170  triun  4200  issod  4416  frirrg  4447  frind  4449  peano2  4693  dmmptd  5463  fun11iun  5604  fniinfv  5704  eqfnfv  5744  eqfnfvd  5747  fnmptfvd  5751  dff3im  5792  dffo4  5795  fmptd  5801  ffnfv  5805  fmpt2d  5809  ffvresb  5810  funiun  5828  fconst2g  5868  fconstfvm  5871  resfunexg  5874  eufnfv  5884  foco2  5893  fniunfv  5902  fcofo  5924  fliftel  5933  fliftfun  5936  fliftfuns  5938  riota5f  5997  f1ocnvd  6224  suppssov1  6231  offval2  6250  ofrfval2  6251  offveqb  6254  offveq  6255  caofref  6259  caofinvl  6260  caofid0l  6261  caofid0r  6262  caofid1  6263  caofid2  6264  opabex3d  6282  uchoice  6299  oprssdmm  6333  f1od2  6399  disjxp1  6400  tfrlem1  6473  tfrlemisucaccv  6490  tfrlemiubacc  6495  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemubacc  6511  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemubacc  6524  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  rdgon  6551  freccllem  6567  frecfcllem  6569  omcl  6628  oeicl  6629  qliftfuns  6787  ixpeq2dva  6881  xpf1o  7029  mapxpen  7033  isinfinf  7085  fimax2gtrilemstep  7089  undifdcss  7114  opabfi  7131  eqsuptid  7195  eqinftid  7219  difinfsnlem  7297  difinfsn  7298  ctmlemr  7306  ctm  7307  ctssdclemn0  7308  ctssdccl  7309  enumctlemm  7312  nninfninc  7321  nnnninf  7324  nnnninfeq  7326  enomnilem  7336  ismkvnex  7353  enmkvlem  7359  enwomnilem  7367  nninfwlporlemd  7370  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  nninfwlpoim  7377  nninfinfwlpo  7378  finacn  7418  acfun  7421  exmidaclem  7422  exmidontriimlem4  7438  exmidontriim  7439  pw1on  7443  ccfunen  7482  cc2lem  7484  cc3  7486  acnccim  7490  genprndl  7740  genprndu  7741  nqprloc  7764  ltexprlemrnd  7824  ltexprlemdisj  7825  lteupri  7836  recexprlemrnd  7848  recexprlemdisj  7849  caucvgprlemlim  7900  caucvgprprlemlim  7930  suplocexprlemml  7935  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  caucvgsrlembound  8013  caucvgsrlemgt1  8014  caucvgsrlemoffgt1  8018  caucvgsr  8021  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  elrealeu  8048  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  negeu  8369  eqord1  8662  eqord2  8663  creur  9138  creui  9139  suprzclex  9577  supinfneg  9828  infsupneg  9829  infregelbex  9831  indstr2  9842  iooidg  10143  iccsupr  10200  icoshftf1o  10225  fznlem  10275  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  zsupssdc  10497  exbtwnzlemstep  10506  exbtwnzlemex  10508  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgtcl  10673  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgfunlem  10680  frecuzrdgsuctlem  10684  nninfinf  10704  iseqovex  10719  seq3val  10721  seqvalcd  10722  seq3-1  10723  seqf  10725  seq3p1  10726  seqovcd  10728  seqp1cd  10731  seq3clss  10732  seq3fveq2  10736  seqfveq2g  10738  seqfveqg  10739  seq3fveq  10740  seq3feq  10741  seq3shft2  10742  seqshft2g  10743  monoord  10746  monoord2  10747  ser3mono  10748  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3caopr2  10754  seqcaopr2g  10755  iseqf1olemqk  10768  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  seqf1og  10782  seq3id3  10785  seq3id  10786  seq3id2  10787  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  ser3ge0  10797  nn0ltexp2  10970  bccl  11028  hashinfuni  11038  hashennnuni  11040  wrdexg  11123  ccatlen  11171  ccatvalfn  11177  ccatrn  11185  swrdlen  11232  swrdwrdsymbg  11244  swrdswrd  11285  wrdind  11302  reuccatpfxs1  11327  shftf  11390  seq3shft  11398  caucvgrelemcau  11540  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemcvg  11579  resqrexlemglsq  11582  resqrexlemga  11583  maxabslemval  11768  negfi  11788  minmax  11790  xrmaxiflemval  11810  xrminmax  11825  climconst  11850  2clim  11861  climcn1  11868  climcn2  11869  reccn2ap  11873  cn1lem  11874  climsqz  11895  climsqz2  11896  climcau  11907  climrecvg1n  11908  serf0  11912  sumeq2dv  11928  sumrbdclem  11937  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  zsumdc  11944  isum  11945  fsumgcl  11946  fsum3  11947  fsumf1o  11950  isumss  11951  fisumss  11952  isumss2  11953  fsum3cvg2  11954  fsumsersdc  11955  fsum3ser  11957  fsumcl2lem  11958  fsumadd  11966  fsumsplit  11967  fsumm1  11976  fsum1p  11978  isumclim3  11983  isummulc2  11986  sumsplitdc  11992  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fsummulc2  12008  fsumge1  12021  fsum00  12022  fsumabs  12025  telfsumo  12026  telfsumo2  12027  fsumparts  12030  fsumrelem  12031  fsumiun  12037  hashiun  12038  hash2iun  12039  binomlem  12043  isumshft  12050  isum1p  12052  isumnn0nn  12053  isumrpcl  12054  isumlessdc  12056  divcnv  12057  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratnn  12091  cvgratz  12092  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  clim2prod  12099  prodeq2dv  12126  prodrbdclem  12131  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  iprodap  12140  fprodseq  12143  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodmul  12151  fprodsplit  12157  fprodm1  12158  fprod1p  12159  fprodm1s  12161  fprodp1s  12162  fprodunsn  12164  fprodcl2lem  12165  fprodabs  12176  fprodeq0  12177  fprodap0  12181  fprod2dlemstep  12182  fprodcom2fi  12186  fprodrec  12189  fprodmodd  12201  efcvgfsum  12227  dvdsssfz1  12412  bitsfi  12517  bitsinv1  12522  dvdsbnd  12526  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemle  12578  bezoutlemsup  12579  dfgcd3  12580  dfgcd2  12584  nnwodc  12606  uzwodc  12607  nnwosdc  12609  nninfctlemfo  12610  coprmgcdb  12659  prmdc  12701  isprm5  12713  isprm6  12718  phivalfi  12783  phibndlem  12787  dfphi2  12791  hashdvds  12792  phiprmpw  12793  phimullem  12796  eulerthlemfi  12799  dvdsfi  12810  hashgcdeq  12811  phisum  12812  reumodprminv  12825  pclemdc  12860  pc2dvds  12902  pcz  12904  pcprmpw2  12905  pcmptdvds  12917  pcprod  12918  pcfac  12922  qexpz  12924  prmpwdvds  12927  pockthg  12929  infpnlem2  12932  1arithlem4  12938  1arith  12939  4sqlemafi  12967  4sqlemffi  12968  4sqleminfi  12969  ennnfonelemex  13034  ennnfonelemfun  13037  ennnfonelemf1  13038  ennnfonelemnn0  13042  ennnfonelemim  13044  exmidunben  13046  ctinfomlemom  13047  ctinfom  13048  ctinf  13050  ctiunctlemudc  13057  ctiunctlemf  13058  ctiunctlemfo  13059  omctfn  13063  ssnnctlemct  13066  nninfdclemcl  13068  nninfdclemp1  13070  pwsbas  13374  imasival  13388  ismgmid2  13462  mgmidsssn0  13466  grpinvalem  13467  grpinva  13468  gsumress  13477  issgrpd  13494  prdsplusgsgrpcl  13496  sgrpidmndm  13502  ismndd  13519  mndpfo  13520  prdsplusgcl  13528  prdsidlem  13529  mhmima  13573  mhmeql  13574  gsumvallem2  13575  isgrpd2e  13602  dfgrp2  13609  grpidd2  13623  isgrpinv  13636  grplrinv  13639  grpidinv  13641  dfgrp3me  13682  prdsinvlem  13690  mhmmnd  13702  ghmgrp  13704  mulgsubcl  13722  issubg2m  13775  issubgrpd2  13776  grpissubg  13780  subgintm  13784  nmzsubg  13796  ssnmz  13797  ghmrn  13843  ghmeql  13853  ghmf1  13859  conjnmz  13865  conjnmzb  13866  rinvmod  13895  srgrz  13996  srglz  13997  srgisid  13998  ringsrg  14059  rhmdvdsr  14188  rhmopp  14189  subrngintm  14225  subrg1  14244  subrgugrp  14253  subrgintm  14256  unitrrg  14280  aprap  14299  islmodd  14306  lssuni  14376  lsssubg  14390  lssintclm  14397  dflidl2rng  14494  lidlsubg  14499  cnsubglem  14592  gsumfzfsumlemm  14600  znf1o  14664  znidomb  14671  psrbagfi  14686  psr1clfi  14701  mplsubgfilemm  14711  mplsubgfilemcl  14712  mplsubgfi  14714  fiinbas  14772  tgclb  14788  restbasg  14891  iscnp4  14941  cnco  14944  cnptopco  14945  cnss1  14949  cnss2  14950  cncnpi  14951  cncnp  14953  cnconst2  14956  cnrest  14958  cnptopresti  14961  cnpdis  14965  lmtopcnp  14973  txbasval  14990  tx1cn  14992  tx2cn  14993  txcnp  14994  upxp  14995  txdis1cn  15001  cnmpt11  15006  psmet0  15050  psmettri2  15051  psmetxrge0  15055  psmetres2  15056  ismeti  15069  xmetpsmet  15092  blsscls2  15216  comet  15222  xmettx  15233  tgioo  15277  tgqioo  15278  fsumcncntop  15290  elcncf1di  15302  cdivcncfap  15327  mulcncflem  15330  mulcncf  15331  cnopnap  15334  divcncfap  15337  dedekindeulemuub  15340  dedekindeulemlu  15344  suplociccreex  15347  suplociccex  15348  dedekindicclemuub  15349  dedekindicclemlu  15353  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemdisj  15363  ivthinclemloc  15364  ivthinc  15366  ivthdec  15367  dich0  15375  ivthdich  15376  cnplimclemr  15392  limccnp2cntop  15400  limccoap  15401  dvcn  15423  dvfre  15433  dvrecap  15436  dvmptclx  15441  dvmptaddx  15442  dvmptmulx  15443  dveflem  15449  dvef  15450  ply1termlem  15465  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plycj  15484  plyreres  15487  dvply1  15488  sin0pilem1  15504  sin0pilem2  15505  mpodvdsmulf1o  15713  mersenne  15720  perfectlem2  15723  lgsval2lem  15738  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1f1o  15788  gausslemma2dlem2  15790  gausslemma2dlem3  15791  lgsquadlemofi  15804  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1a1  15814  2sqlem6  15848  2sqlem8  15851  2sqlem10  15853  usgruspgrben  16036  uspgredg2v  16071  usgredg2v  16074  subuhgr  16122  subupgr  16123  subumgr  16124  subusgr  16125  vtxedgfi  16139  vtxlpfi  16140  wlk1walkdom  16209  wlkres  16229  fnmptd  16400  bj-charfun  16402  bj-charfundc  16403  bj-charfunr  16405  2omap  16594  pw1nct  16604  nnsf  16607  nninfalllem1  16610  nninfall  16611  nninfself  16615  nninfsellemeq  16616  nninfsellemeqinf  16618  nninfsel  16619  nnnninfex  16624  nninfnfiinf  16625  isomninnlem  16634  trilpolemeq1  16644  trilpo  16647  apdiff  16652  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  redcwlpo  16659  redc0  16661  reap0  16662  dceqnconst  16664  dcapnconst  16665  nconstwlpolem  16669  nconstwlpo  16670  neapmkv  16672  ltlenmkv  16674