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  2653  rabbidva  2764  ssrabdv  3280  ss2rabdv  3282  iuneq2dv  3962  iunssd  3987  disjeq2dv  4040  mpteq12dva  4141  triun  4171  issod  4384  frirrg  4415  frind  4417  peano2  4661  dmmptd  5426  fun11iun  5565  fniinfv  5660  eqfnfv  5700  eqfnfvd  5703  fnmptfvd  5707  dff3im  5748  dffo4  5751  fmptd  5757  ffnfv  5761  fmpt2d  5765  ffvresb  5766  funiun  5784  fconst2g  5822  fconstfvm  5825  resfunexg  5828  eufnfv  5838  foco2  5845  fniunfv  5854  fcofo  5876  fliftel  5885  fliftfun  5888  fliftfuns  5890  riota5f  5947  f1ocnvd  6171  suppssov1  6178  offval2  6197  ofrfval2  6198  offveqb  6201  offveq  6202  caofref  6206  caofinvl  6207  caofid0l  6208  caofid0r  6209  caofid1  6210  caofid2  6211  opabex3d  6229  uchoice  6246  oprssdmm  6280  f1od2  6344  disjxp1  6345  tfrlem1  6417  tfrlemisucaccv  6434  tfrlemiubacc  6439  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemubacc  6455  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemubacc  6468  tfrcllemaccex  6470  tfrcllemres  6471  tfrcl  6473  rdgon  6495  freccllem  6511  frecfcllem  6513  omcl  6570  oeicl  6571  qliftfuns  6729  ixpeq2dva  6823  xpf1o  6966  mapxpen  6970  isinfinf  7020  fimax2gtrilemstep  7023  undifdcss  7046  opabfi  7061  eqsuptid  7125  eqinftid  7149  difinfsnlem  7227  difinfsn  7228  ctmlemr  7236  ctm  7237  ctssdclemn0  7238  ctssdccl  7239  enumctlemm  7242  nninfninc  7251  nnnninf  7254  nnnninfeq  7256  enomnilem  7266  ismkvnex  7283  enmkvlem  7289  enwomnilem  7297  nninfwlporlemd  7300  nninfwlpoimlemg  7303  nninfwlpoimlemginf  7304  nninfwlpoim  7307  nninfinfwlpo  7308  finacn  7347  acfun  7350  exmidaclem  7351  exmidontriimlem4  7367  exmidontriim  7368  pw1on  7372  ccfunen  7411  cc2lem  7413  cc3  7415  acnccim  7419  genprndl  7669  genprndu  7670  nqprloc  7693  ltexprlemrnd  7753  ltexprlemdisj  7754  lteupri  7765  recexprlemrnd  7777  recexprlemdisj  7778  caucvgprlemlim  7829  caucvgprprlemlim  7859  suplocexprlemml  7864  suplocexprlemrl  7865  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  caucvgsrlembound  7942  caucvgsrlemgt1  7943  caucvgsrlemoffgt1  7947  caucvgsr  7950  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  elrealeu  7977  axcaucvglemcau  8046  axcaucvglemres  8047  axpre-suploclemres  8049  negeu  8298  eqord1  8591  eqord2  8592  creur  9067  creui  9068  suprzclex  9506  supinfneg  9751  infsupneg  9752  infregelbex  9754  indstr2  9765  iooidg  10066  iccsupr  10123  icoshftf1o  10148  fznlem  10198  exfzdc  10406  zsupcllemstep  10409  infssuzex  10413  suprzubdc  10416  zsupssdc  10418  exbtwnzlemstep  10427  exbtwnzlemex  10429  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgtcl  10594  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgfunlem  10601  frecuzrdgsuctlem  10605  nninfinf  10625  iseqovex  10640  seq3val  10642  seqvalcd  10643  seq3-1  10644  seqf  10646  seq3p1  10647  seqovcd  10649  seqp1cd  10652  seq3clss  10653  seq3fveq2  10657  seqfveq2g  10659  seqfveqg  10660  seq3fveq  10661  seq3feq  10662  seq3shft2  10663  seqshft2g  10664  monoord  10667  monoord2  10668  ser3mono  10669  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seq3caopr2  10675  seqcaopr2g  10676  iseqf1olemqk  10689  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  iseqf1olemfvp  10692  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seq3f1oleml  10698  seq3f1o  10699  seqf1og  10703  seq3id3  10706  seq3id  10707  seq3id2  10708  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  ser3ge0  10718  nn0ltexp2  10891  bccl  10949  hashinfuni  10959  hashennnuni  10961  wrdexg  11042  ccatlen  11089  ccatvalfn  11095  ccatrn  11103  swrdlen  11143  swrdwrdsymbg  11155  swrdswrd  11196  wrdind  11213  reuccatpfxs1  11238  shftf  11256  seq3shft  11264  caucvgrelemcau  11406  cvg1nlemcau  11410  cvg1nlemres  11411  resqrexlemcvg  11445  resqrexlemglsq  11448  resqrexlemga  11449  maxabslemval  11634  negfi  11654  minmax  11656  xrmaxiflemval  11676  xrminmax  11691  climconst  11716  2clim  11727  climcn1  11734  climcn2  11735  reccn2ap  11739  cn1lem  11740  climsqz  11761  climsqz2  11762  climcau  11773  climrecvg1n  11774  serf0  11778  sumeq2dv  11794  sumrbdclem  11803  fsum3cvg  11804  summodclem3  11806  summodclem2a  11807  zsumdc  11810  isum  11811  fsumgcl  11812  fsum3  11813  fsumf1o  11816  isumss  11817  fisumss  11818  isumss2  11819  fsum3cvg2  11820  fsumsersdc  11821  fsum3ser  11823  fsumcl2lem  11824  fsumadd  11832  fsumsplit  11833  fsumm1  11842  fsum1p  11844  isumclim3  11849  isummulc2  11852  sumsplitdc  11858  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fsummulc2  11874  fsumge1  11887  fsum00  11888  fsumabs  11891  telfsumo  11892  telfsumo2  11893  fsumparts  11896  fsumrelem  11897  fsumiun  11903  hashiun  11904  hash2iun  11905  binomlem  11909  isumshft  11916  isum1p  11918  isumnn0nn  11919  isumrpcl  11920  isumlessdc  11922  divcnv  11923  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemseq  11952  cvgratnnlemabsle  11953  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  clim2prod  11965  prodeq2dv  11992  prodrbdclem  11997  fproddccvg  11998  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  iprodap  12006  fprodseq  12009  fprodf1o  12014  prodssdc  12015  fprodssdc  12016  fprodmul  12017  fprodsplit  12023  fprodm1  12024  fprod1p  12025  fprodm1s  12027  fprodp1s  12028  fprodunsn  12030  fprodcl2lem  12031  fprodabs  12042  fprodeq0  12043  fprodap0  12047  fprod2dlemstep  12048  fprodcom2fi  12052  fprodrec  12055  fprodmodd  12067  efcvgfsum  12093  dvdsssfz1  12278  bitsfi  12383  bitsinv1  12388  dvdsbnd  12392  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlemle  12444  bezoutlemsup  12445  dfgcd3  12446  dfgcd2  12450  nnwodc  12472  uzwodc  12473  nnwosdc  12475  nninfctlemfo  12476  coprmgcdb  12525  prmdc  12567  isprm5  12579  isprm6  12584  phivalfi  12649  phibndlem  12653  dfphi2  12657  hashdvds  12658  phiprmpw  12659  phimullem  12662  eulerthlemfi  12665  dvdsfi  12676  hashgcdeq  12677  phisum  12678  reumodprminv  12691  pclemdc  12726  pc2dvds  12768  pcz  12770  pcprmpw2  12771  pcmptdvds  12783  pcprod  12784  pcfac  12788  qexpz  12790  prmpwdvds  12793  pockthg  12795  infpnlem2  12798  1arithlem4  12804  1arith  12805  4sqlemafi  12833  4sqlemffi  12834  4sqleminfi  12835  ennnfonelemex  12900  ennnfonelemfun  12903  ennnfonelemf1  12904  ennnfonelemnn0  12908  ennnfonelemim  12910  exmidunben  12912  ctinfomlemom  12913  ctinfom  12914  ctinf  12916  ctiunctlemudc  12923  ctiunctlemf  12924  ctiunctlemfo  12925  omctfn  12929  ssnnctlemct  12932  nninfdclemcl  12934  nninfdclemp1  12936  pwsbas  13239  imasival  13253  ismgmid2  13327  mgmidsssn0  13331  grpinvalem  13332  grpinva  13333  gsumress  13342  issgrpd  13359  prdsplusgsgrpcl  13361  sgrpidmndm  13367  ismndd  13384  mndpfo  13385  prdsplusgcl  13393  prdsidlem  13394  mhmima  13438  mhmeql  13439  gsumvallem2  13440  isgrpd2e  13467  dfgrp2  13474  grpidd2  13488  isgrpinv  13501  grplrinv  13504  grpidinv  13506  dfgrp3me  13547  prdsinvlem  13555  mhmmnd  13567  ghmgrp  13569  mulgsubcl  13587  issubg2m  13640  issubgrpd2  13641  grpissubg  13645  subgintm  13649  nmzsubg  13661  ssnmz  13662  ghmrn  13708  ghmeql  13718  ghmf1  13724  conjnmz  13730  conjnmzb  13731  rinvmod  13760  srgrz  13861  srglz  13862  srgisid  13863  ringsrg  13924  rhmdvdsr  14052  rhmopp  14053  subrngintm  14089  subrg1  14108  subrgugrp  14117  subrgintm  14120  unitrrg  14144  aprap  14163  islmodd  14170  lssuni  14240  lsssubg  14254  lssintclm  14261  dflidl2rng  14358  lidlsubg  14363  cnsubglem  14456  gsumfzfsumlemm  14464  znf1o  14528  znidomb  14535  psrbagfi  14550  psr1clfi  14565  mplsubgfilemm  14575  mplsubgfilemcl  14576  mplsubgfi  14578  fiinbas  14636  tgclb  14652  restbasg  14755  iscnp4  14805  cnco  14808  cnptopco  14809  cnss1  14813  cnss2  14814  cncnpi  14815  cncnp  14817  cnconst2  14820  cnrest  14822  cnptopresti  14825  cnpdis  14829  lmtopcnp  14837  txbasval  14854  tx1cn  14856  tx2cn  14857  txcnp  14858  upxp  14859  txdis1cn  14865  cnmpt11  14870  psmet0  14914  psmettri2  14915  psmetxrge0  14919  psmetres2  14920  ismeti  14933  xmetpsmet  14956  blsscls2  15080  comet  15086  xmettx  15097  tgioo  15141  tgqioo  15142  fsumcncntop  15154  elcncf1di  15166  cdivcncfap  15191  mulcncflem  15194  mulcncf  15195  cnopnap  15198  divcncfap  15201  dedekindeulemuub  15204  dedekindeulemlu  15208  suplociccreex  15211  suplociccex  15212  dedekindicclemuub  15213  dedekindicclemlu  15217  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemdisj  15227  ivthinclemloc  15228  ivthinc  15230  ivthdec  15231  dich0  15239  ivthdich  15240  cnplimclemr  15256  limccnp2cntop  15264  limccoap  15265  dvcn  15287  dvfre  15297  dvrecap  15300  dvmptclx  15305  dvmptaddx  15306  dvmptmulx  15307  dveflem  15313  dvef  15314  ply1termlem  15329  plyaddlem1  15334  plymullem1  15335  plycoeid3  15344  plycj  15348  plyreres  15351  dvply1  15352  sin0pilem1  15368  sin0pilem2  15369  mpodvdsmulf1o  15577  mersenne  15584  perfectlem2  15587  lgsval2lem  15602  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1f1o  15652  gausslemma2dlem2  15654  gausslemma2dlem3  15655  lgsquadlemofi  15668  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1a1  15678  2sqlem6  15712  2sqlem8  15715  2sqlem10  15717  fnmptd  15940  bj-charfun  15942  bj-charfundc  15943  bj-charfunr  15945  2omap  16132  pw1nct  16142  nnsf  16144  nninfalllem1  16147  nninfall  16148  nninfself  16152  nninfsellemeq  16153  nninfsellemeqinf  16155  nninfsel  16156  nnnninfex  16161  nninfnfiinf  16162  isomninnlem  16171  trilpolemeq1  16181  trilpo  16184  apdiff  16189  iswomninnlem  16190  iswomni0  16192  ismkvnnlem  16193  redcwlpo  16196  redc0  16198  reap0  16199  dceqnconst  16201  dcapnconst  16202  nconstwlpolem  16206  nconstwlpo  16207  neapmkv  16209  ltlenmkv  16211