Theorem ralrimiva 2606

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  ralrimivvva  2616  rgen2  2619  rgen3  2620  nrexdv  2626  r19.29vva  2679  rabbidva  2791  ssrabdv  3307  ss2rabdv  3309  iuneq2dv  3996  iunssd  4021  disjeq2dv  4074  mpteq12dva  4175  triun  4205  issod  4422  frirrg  4453  frind  4455  peano2  4699  dmmptd  5470  fun11iun  5613  fniinfv  5713  eqfnfv  5753  eqfnfvd  5756  fnmptfvd  5760  dff3im  5800  dffo4  5803  fmptd  5809  ffnfv  5813  fmpt2d  5817  ffvresb  5818  funiun  5837  fconst2g  5877  fconstfvm  5880  resfunexg  5883  eufnfv  5895  foco2  5904  fniunfv  5913  fcofo  5935  fliftel  5944  fliftfun  5947  fliftfuns  5949  riota5f  6008  f1ocnvd  6235  suppssov1  6241  offval2  6260  ofrfval2  6261  offveqb  6264  offveq  6265  caofref  6269  caofinvl  6270  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  opabex3d  6292  uchoice  6309  oprssdmm  6343  f1od2  6409  disjxp1  6410  funsssuppss  6436  suppofss1dcl  6442  suppofss2dcl  6443  tfrlem1  6517  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemubacc  6555  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemubacc  6568  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  rdgon  6595  freccllem  6611  frecfcllem  6613  omcl  6672  oeicl  6673  qliftfuns  6831  ixpeq2dva  6925  xpf1o  7073  mapxpen  7077  isinfinf  7129  fimax2gtrilemstep  7133  undifdcss  7158  opabfi  7175  eqsuptid  7256  eqinftid  7280  difinfsnlem  7358  difinfsn  7359  ctmlemr  7367  ctm  7368  ctssdclemn0  7369  ctssdccl  7370  enumctlemm  7373  nninfninc  7382  nnnninf  7385  nnnninfeq  7387  enomnilem  7397  ismkvnex  7414  enmkvlem  7420  enwomnilem  7428  nninfwlporlemd  7431  nninfwlpoimlemg  7434  nninfwlpoimlemginf  7435  nninfwlpoim  7438  nninfinfwlpo  7439  finacn  7479  acfun  7482  exmidaclem  7483  exmidontriimlem4  7499  exmidontriim  7500  pw1on  7504  ccfunen  7543  cc2lem  7545  cc3  7547  acnccim  7551  genprndl  7801  genprndu  7802  nqprloc  7825  ltexprlemrnd  7885  ltexprlemdisj  7886  lteupri  7897  recexprlemrnd  7909  recexprlemdisj  7910  caucvgprlemlim  7961  caucvgprprlemlim  7991  suplocexprlemml  7996  suplocexprlemrl  7997  suplocexprlemmu  7998  suplocexprlemru  7999  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemub  8003  caucvgsrlembound  8074  caucvgsrlemgt1  8075  caucvgsrlemoffgt1  8079  caucvgsr  8082  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  elrealeu  8109  axcaucvglemcau  8178  axcaucvglemres  8179  axpre-suploclemres  8181  negeu  8429  eqord1  8722  eqord2  8723  creur  9198  creui  9199  suprzclex  9639  supinfneg  9890  infsupneg  9891  infregelbex  9893  indstr2  9904  iooidg  10205  iccsupr  10262  icoshftf1o  10287  fznlem  10338  exfzdc  10549  zsupcllemstep  10552  infssuzex  10556  suprzubdc  10559  zsupssdc  10561  exbtwnzlemstep  10570  exbtwnzlemex  10572  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgtcl  10737  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  frecuzrdgfunlem  10744  frecuzrdgsuctlem  10748  nninfinf  10768  iseqovex  10783  seq3val  10785  seqvalcd  10786  seq3-1  10787  seqf  10789  seq3p1  10790  seqovcd  10792  seqp1cd  10795  seq3clss  10796  seq3fveq2  10800  seqfveq2g  10802  seqfveqg  10803  seq3fveq  10804  seq3feq  10805  seq3shft2  10806  seqshft2g  10807  monoord  10810  monoord2  10811  ser3mono  10812  seq3split  10813  seqsplitg  10814  seq3caopr3  10816  seqcaopr3g  10817  seq3caopr2  10818  seqcaopr2g  10819  iseqf1olemqk  10832  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  iseqf1olemfvp  10835  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seq3f1oleml  10841  seq3f1o  10842  seqf1og  10846  seq3id3  10849  seq3id  10850  seq3id2  10851  seq3homo  10852  seq3z  10853  seqhomog  10855  seqfeq4g  10856  ser3ge0  10861  nn0ltexp2  11034  bccl  11092  hashinfuni  11102  hashennnuni  11104  wrdexg  11190  ccatlen  11238  ccatvalfn  11244  ccatrn  11252  swrdlen  11299  swrdwrdsymbg  11311  swrdswrd  11352  wrdind  11369  reuccatpfxs1  11394  shftf  11470  seq3shft  11478  caucvgrelemcau  11620  cvg1nlemcau  11624  cvg1nlemres  11625  resqrexlemcvg  11659  resqrexlemglsq  11662  resqrexlemga  11663  maxabslemval  11848  negfi  11868  minmax  11870  xrmaxiflemval  11890  xrminmax  11905  climconst  11930  2clim  11941  climcn1  11948  climcn2  11949  reccn2ap  11953  cn1lem  11954  climsqz  11975  climsqz2  11976  climcau  11987  climrecvg1n  11988  serf0  11992  sumeq2dv  12008  sumrbdclem  12018  fsum3cvg  12019  summodclem3  12021  summodclem2a  12022  zsumdc  12025  isum  12026  fsumgcl  12027  fsum3  12028  fsumf1o  12031  isumss  12032  fisumss  12033  isumss2  12034  fsum3cvg2  12035  fsumsersdc  12036  fsum3ser  12038  fsumcl2lem  12039  fsumadd  12047  fsumsplit  12048  fsumm1  12057  fsum1p  12059  isumclim3  12064  isummulc2  12067  sumsplitdc  12073  fsum2dlemstep  12075  fisumcom2  12079  fsumshftm  12086  fsummulc2  12089  fsumge1  12102  fsum00  12103  fsumabs  12106  telfsumo  12107  telfsumo2  12108  fsumparts  12111  fsumrelem  12112  fsumiun  12118  hashiun  12119  hash2iun  12120  binomlem  12124  isumshft  12131  isum1p  12133  isumnn0nn  12134  isumrpcl  12135  isumlessdc  12137  divcnv  12138  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratnnlemseq  12167  cvgratnnlemabsle  12168  cvgratnnlemfm  12170  cvgratnnlemrate  12171  cvgratnn  12172  cvgratz  12173  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  clim2prod  12180  prodeq2dv  12207  prodrbdclem  12212  fproddccvg  12213  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  iprodap  12221  fprodseq  12224  fprodf1o  12229  prodssdc  12230  fprodssdc  12231  fprodmul  12232  fprodsplit  12238  fprodm1  12239  fprod1p  12240  fprodm1s  12242  fprodp1s  12243  fprodunsn  12245  fprodcl2lem  12246  fprodabs  12257  fprodeq0  12258  fprodap0  12262  fprod2dlemstep  12263  fprodcom2fi  12267  fprodrec  12270  fprodmodd  12282  efcvgfsum  12308  dvdsssfz1  12493  bitsfi  12598  bitsinv1  12603  dvdsbnd  12607  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemle  12659  bezoutlemsup  12660  dfgcd3  12661  dfgcd2  12665  nnwodc  12687  uzwodc  12688  nnwosdc  12690  nninfctlemfo  12691  coprmgcdb  12740  prmdc  12782  isprm5  12794  isprm6  12799  phivalfi  12864  phibndlem  12868  dfphi2  12872  hashdvds  12873  phiprmpw  12874  phimullem  12877  eulerthlemfi  12880  dvdsfi  12891  hashgcdeq  12892  phisum  12893  reumodprminv  12906  pclemdc  12941  pc2dvds  12983  pcz  12985  pcprmpw2  12986  pcmptdvds  12998  pcprod  12999  pcfac  13003  qexpz  13005  prmpwdvds  13008  pockthg  13010  infpnlem2  13013  1arithlem4  13019  1arith  13020  4sqlemafi  13048  4sqlemffi  13049  4sqleminfi  13050  ennnfonelemex  13115  ennnfonelemfun  13118  ennnfonelemf1  13119  ennnfonelemnn0  13123  ennnfonelemim  13125  exmidunben  13127  ctinfomlemom  13128  ctinfom  13129  ctinf  13131  ctiunctlemudc  13138  ctiunctlemf  13139  ctiunctlemfo  13140  omctfn  13144  ssnnctlemct  13147  nninfdclemcl  13149  nninfdclemp1  13151  pwsbas  13455  imasival  13469  ismgmid2  13543  mgmidsssn0  13547  grpinvalem  13548  grpinva  13549  gsumress  13558  issgrpd  13575  prdsplusgsgrpcl  13577  sgrpidmndm  13583  ismndd  13600  mndpfo  13601  prdsplusgcl  13609  prdsidlem  13610  mhmima  13654  mhmeql  13655  gsumvallem2  13656  isgrpd2e  13683  dfgrp2  13690  grpidd2  13704  isgrpinv  13717  grplrinv  13720  grpidinv  13722  dfgrp3me  13763  prdsinvlem  13771  mhmmnd  13783  ghmgrp  13785  mulgsubcl  13803  issubg2m  13856  issubgrpd2  13857  grpissubg  13861  subgintm  13865  nmzsubg  13877  ssnmz  13878  ghmrn  13924  ghmeql  13934  ghmf1  13940  conjnmz  13946  conjnmzb  13947  rinvmod  13976  srgrz  14078  srglz  14079  srgisid  14080  ringsrg  14141  rhmdvdsr  14270  rhmopp  14271  subrngintm  14307  subrg1  14326  subrgugrp  14335  subrgintm  14338  rrgsupp  14361  unitrrg  14363  aprap  14382  islmodd  14389  lssuni  14459  lsssubg  14473  lssintclm  14480  dflidl2rng  14577  lidlsubg  14582  cnsubglem  14675  gsumfzfsumlemm  14683  znf1o  14747  znidomb  14754  psrbagfi  14770  psrbaglecl  14771  psrbagcon  14772  psr1clfi  14789  mplsubgfilemm  14799  mplsubgfilemcl  14800  mplsubgfi  14802  fiinbas  14860  tgclb  14876  restbasg  14979  iscnp4  15029  cnco  15032  cnptopco  15033  cnss1  15037  cnss2  15038  cncnpi  15039  cncnp  15041  cnconst2  15044  cnrest  15046  cnptopresti  15049  cnpdis  15053  lmtopcnp  15061  txbasval  15078  tx1cn  15080  tx2cn  15081  txcnp  15082  upxp  15083  txdis1cn  15089  cnmpt11  15094  psmet0  15138  psmettri2  15139  psmetxrge0  15143  psmetres2  15144  ismeti  15157  xmetpsmet  15180  blsscls2  15304  comet  15310  xmettx  15321  tgioo  15365  tgqioo  15366  fsumcncntop  15378  elcncf1di  15390  cdivcncfap  15415  mulcncflem  15418  mulcncf  15419  cnopnap  15422  divcncfap  15425  dedekindeulemuub  15428  dedekindeulemlu  15432  suplociccreex  15435  suplociccex  15436  dedekindicclemuub  15437  dedekindicclemlu  15441  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemdisj  15451  ivthinclemloc  15452  ivthinc  15454  ivthdec  15455  dich0  15463  ivthdich  15464  cnplimclemr  15480  limccnp2cntop  15488  limccoap  15489  dvcn  15511  dvfre  15521  dvrecap  15524  dvmptclx  15529  dvmptaddx  15530  dvmptmulx  15531  dveflem  15537  dvef  15538  ply1termlem  15553  plyaddlem1  15558  plymullem1  15559  plycoeid3  15568  plycj  15572  plyreres  15575  dvply1  15576  sin0pilem1  15592  sin0pilem2  15593  mpodvdsmulf1o  15804  mersenne  15811  perfectlem2  15814  lgsval2lem  15829  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem1f1o  15879  gausslemma2dlem2  15881  gausslemma2dlem3  15882  lgsquadlemofi  15895  lgsquadlem1  15896  lgsquadlem2  15897  2lgslem1a1  15905  2sqlem6  15939  2sqlem8  15942  2sqlem10  15944  usgruspgrben  16127  uspgredg2v  16162  usgredg2v  16165  subuhgr  16213  subupgr  16214  subumgr  16215  subusgr  16216  vtxedgfi  16230  vtxlpfi  16231  wlk1walkdom  16300  wlkres  16320  eupth2lembfi  16418  depindlem1  16447  depindlem2  16448  depindlem3  16449  fnmptd  16522  bj-charfun  16523  bj-charfundc  16524  bj-charfunr  16526  2omap  16715  pw1nct  16725  nnsf  16731  nninfalllem1  16734  nninfall  16735  nninfself  16739  nninfsellemeq  16740  nninfsellemeqinf  16742  nninfsel  16743  nnnninfex  16748  nninfnfiinf  16749  repiecef  16760  isomninnlem  16762  trilpolemeq1  16772  trilpo  16775  apdiff  16780  iswomninnlem  16782  iswomni0  16784  ismkvnnlem  16785  redcwlpo  16788  redc0  16790  reap0  16791  dceqnconst  16793  dcapnconst  16794  nconstwlpolem  16798  nconstwlpo  16799  neapmkv  16801  ltlenmkv  16803