Theorem ralrimiva 2603

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralrimivvva  2613  rgen2  2616  rgen3  2617  nrexdv  2623  r19.29vva  2676  rabbidva  2787  ssrabdv  3303  ss2rabdv  3305  iuneq2dv  3986  iunssd  4011  disjeq2dv  4064  mpteq12dva  4165  triun  4195  issod  4410  frirrg  4441  frind  4443  peano2  4687  dmmptd  5454  fun11iun  5595  fniinfv  5694  eqfnfv  5734  eqfnfvd  5737  fnmptfvd  5741  dff3im  5782  dffo4  5785  fmptd  5791  ffnfv  5795  fmpt2d  5799  ffvresb  5800  funiun  5818  fconst2g  5858  fconstfvm  5861  resfunexg  5864  eufnfv  5874  foco2  5883  fniunfv  5892  fcofo  5914  fliftel  5923  fliftfun  5926  fliftfuns  5928  riota5f  5987  f1ocnvd  6214  suppssov1  6221  offval2  6240  ofrfval2  6241  offveqb  6244  offveq  6245  caofref  6249  caofinvl  6250  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  opabex3d  6272  uchoice  6289  oprssdmm  6323  f1od2  6387  disjxp1  6388  tfrlem1  6460  tfrlemisucaccv  6477  tfrlemiubacc  6482  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemubacc  6498  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemubacc  6511  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  rdgon  6538  freccllem  6554  frecfcllem  6556  omcl  6615  oeicl  6616  qliftfuns  6774  ixpeq2dva  6868  xpf1o  7013  mapxpen  7017  isinfinf  7067  fimax2gtrilemstep  7071  undifdcss  7096  opabfi  7111  eqsuptid  7175  eqinftid  7199  difinfsnlem  7277  difinfsn  7278  ctmlemr  7286  ctm  7287  ctssdclemn0  7288  ctssdccl  7289  enumctlemm  7292  nninfninc  7301  nnnninf  7304  nnnninfeq  7306  enomnilem  7316  ismkvnex  7333  enmkvlem  7339  enwomnilem  7347  nninfwlporlemd  7350  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  nninfwlpoim  7357  nninfinfwlpo  7358  finacn  7397  acfun  7400  exmidaclem  7401  exmidontriimlem4  7417  exmidontriim  7418  pw1on  7422  ccfunen  7461  cc2lem  7463  cc3  7465  acnccim  7469  genprndl  7719  genprndu  7720  nqprloc  7743  ltexprlemrnd  7803  ltexprlemdisj  7804  lteupri  7815  recexprlemrnd  7827  recexprlemdisj  7828  caucvgprlemlim  7879  caucvgprprlemlim  7909  suplocexprlemml  7914  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  caucvgsrlembound  7992  caucvgsrlemgt1  7993  caucvgsrlemoffgt1  7997  caucvgsr  8000  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  elrealeu  8027  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  negeu  8348  eqord1  8641  eqord2  8642  creur  9117  creui  9118  suprzclex  9556  supinfneg  9802  infsupneg  9803  infregelbex  9805  indstr2  9816  iooidg  10117  iccsupr  10174  icoshftf1o  10199  fznlem  10249  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  zsupssdc  10470  exbtwnzlemstep  10479  exbtwnzlemex  10481  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgtcl  10646  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgfunlem  10653  frecuzrdgsuctlem  10657  nninfinf  10677  iseqovex  10692  seq3val  10694  seqvalcd  10695  seq3-1  10696  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3clss  10705  seq3fveq2  10709  seqfveq2g  10711  seqfveqg  10712  seq3fveq  10713  seq3feq  10714  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1og  10755  seq3id3  10758  seq3id  10759  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  ser3ge0  10770  nn0ltexp2  10943  bccl  11001  hashinfuni  11011  hashennnuni  11013  wrdexg  11095  ccatlen  11143  ccatvalfn  11149  ccatrn  11157  swrdlen  11200  swrdwrdsymbg  11212  swrdswrd  11253  wrdind  11270  reuccatpfxs1  11295  shftf  11357  seq3shft  11365  caucvgrelemcau  11507  cvg1nlemcau  11511  cvg1nlemres  11512  resqrexlemcvg  11546  resqrexlemglsq  11549  resqrexlemga  11550  maxabslemval  11735  negfi  11755  minmax  11757  xrmaxiflemval  11777  xrminmax  11792  climconst  11817  2clim  11828  climcn1  11835  climcn2  11836  reccn2ap  11840  cn1lem  11841  climsqz  11862  climsqz2  11863  climcau  11874  climrecvg1n  11875  serf0  11879  sumeq2dv  11895  sumrbdclem  11904  fsum3cvg  11905  summodclem3  11907  summodclem2a  11908  zsumdc  11911  isum  11912  fsumgcl  11913  fsum3  11914  fsumf1o  11917  isumss  11918  fisumss  11919  isumss2  11920  fsum3cvg2  11921  fsumsersdc  11922  fsum3ser  11924  fsumcl2lem  11925  fsumadd  11933  fsumsplit  11934  fsumm1  11943  fsum1p  11945  isumclim3  11950  isummulc2  11953  sumsplitdc  11959  fsum2dlemstep  11961  fisumcom2  11965  fsumshftm  11972  fsummulc2  11975  fsumge1  11988  fsum00  11989  fsumabs  11992  telfsumo  11993  telfsumo2  11994  fsumparts  11997  fsumrelem  11998  fsumiun  12004  hashiun  12005  hash2iun  12006  binomlem  12010  isumshft  12017  isum1p  12019  isumnn0nn  12020  isumrpcl  12021  isumlessdc  12023  divcnv  12024  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratnnlemseq  12053  cvgratnnlemabsle  12054  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratnn  12058  cvgratz  12059  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  clim2prod  12066  prodeq2dv  12093  prodrbdclem  12098  fproddccvg  12099  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  iprodap  12107  fprodseq  12110  fprodf1o  12115  prodssdc  12116  fprodssdc  12117  fprodmul  12118  fprodsplit  12124  fprodm1  12125  fprod1p  12126  fprodm1s  12128  fprodp1s  12129  fprodunsn  12131  fprodcl2lem  12132  fprodabs  12143  fprodeq0  12144  fprodap0  12148  fprod2dlemstep  12149  fprodcom2fi  12153  fprodrec  12156  fprodmodd  12168  efcvgfsum  12194  dvdsssfz1  12379  bitsfi  12484  bitsinv1  12489  dvdsbnd  12493  bezoutlemstep  12534  bezoutlemmain  12535  bezoutlemle  12545  bezoutlemsup  12546  dfgcd3  12547  dfgcd2  12551  nnwodc  12573  uzwodc  12574  nnwosdc  12576  nninfctlemfo  12577  coprmgcdb  12626  prmdc  12668  isprm5  12680  isprm6  12685  phivalfi  12750  phibndlem  12754  dfphi2  12758  hashdvds  12759  phiprmpw  12760  phimullem  12763  eulerthlemfi  12766  dvdsfi  12777  hashgcdeq  12778  phisum  12779  reumodprminv  12792  pclemdc  12827  pc2dvds  12869  pcz  12871  pcprmpw2  12872  pcmptdvds  12884  pcprod  12885  pcfac  12889  qexpz  12891  prmpwdvds  12894  pockthg  12896  infpnlem2  12899  1arithlem4  12905  1arith  12906  4sqlemafi  12934  4sqlemffi  12935  4sqleminfi  12936  ennnfonelemex  13001  ennnfonelemfun  13004  ennnfonelemf1  13005  ennnfonelemnn0  13009  ennnfonelemim  13011  exmidunben  13013  ctinfomlemom  13014  ctinfom  13015  ctinf  13017  ctiunctlemudc  13024  ctiunctlemf  13025  ctiunctlemfo  13026  omctfn  13030  ssnnctlemct  13033  nninfdclemcl  13035  nninfdclemp1  13037  pwsbas  13341  imasival  13355  ismgmid2  13429  mgmidsssn0  13433  grpinvalem  13434  grpinva  13435  gsumress  13444  issgrpd  13461  prdsplusgsgrpcl  13463  sgrpidmndm  13469  ismndd  13486  mndpfo  13487  prdsplusgcl  13495  prdsidlem  13496  mhmima  13540  mhmeql  13541  gsumvallem2  13542  isgrpd2e  13569  dfgrp2  13576  grpidd2  13590  isgrpinv  13603  grplrinv  13606  grpidinv  13608  dfgrp3me  13649  prdsinvlem  13657  mhmmnd  13669  ghmgrp  13671  mulgsubcl  13689  issubg2m  13742  issubgrpd2  13743  grpissubg  13747  subgintm  13751  nmzsubg  13763  ssnmz  13764  ghmrn  13810  ghmeql  13820  ghmf1  13826  conjnmz  13832  conjnmzb  13833  rinvmod  13862  srgrz  13963  srglz  13964  srgisid  13965  ringsrg  14026  rhmdvdsr  14155  rhmopp  14156  subrngintm  14192  subrg1  14211  subrgugrp  14220  subrgintm  14223  unitrrg  14247  aprap  14266  islmodd  14273  lssuni  14343  lsssubg  14357  lssintclm  14364  dflidl2rng  14461  lidlsubg  14466  cnsubglem  14559  gsumfzfsumlemm  14567  znf1o  14631  znidomb  14638  psrbagfi  14653  psr1clfi  14668  mplsubgfilemm  14678  mplsubgfilemcl  14679  mplsubgfi  14681  fiinbas  14739  tgclb  14755  restbasg  14858  iscnp4  14908  cnco  14911  cnptopco  14912  cnss1  14916  cnss2  14917  cncnpi  14918  cncnp  14920  cnconst2  14923  cnrest  14925  cnptopresti  14928  cnpdis  14932  lmtopcnp  14940  txbasval  14957  tx1cn  14959  tx2cn  14960  txcnp  14961  upxp  14962  txdis1cn  14968  cnmpt11  14973  psmet0  15017  psmettri2  15018  psmetxrge0  15022  psmetres2  15023  ismeti  15036  xmetpsmet  15059  blsscls2  15183  comet  15189  xmettx  15200  tgioo  15244  tgqioo  15245  fsumcncntop  15257  elcncf1di  15269  cdivcncfap  15294  mulcncflem  15297  mulcncf  15298  cnopnap  15301  divcncfap  15304  dedekindeulemuub  15307  dedekindeulemlu  15311  suplociccreex  15314  suplociccex  15315  dedekindicclemuub  15316  dedekindicclemlu  15320  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemdisj  15330  ivthinclemloc  15331  ivthinc  15333  ivthdec  15334  dich0  15342  ivthdich  15343  cnplimclemr  15359  limccnp2cntop  15367  limccoap  15368  dvcn  15390  dvfre  15400  dvrecap  15403  dvmptclx  15408  dvmptaddx  15409  dvmptmulx  15410  dveflem  15416  dvef  15417  ply1termlem  15432  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  plycj  15451  plyreres  15454  dvply1  15455  sin0pilem1  15471  sin0pilem2  15472  mpodvdsmulf1o  15680  mersenne  15687  perfectlem2  15690  lgsval2lem  15705  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem1f1o  15755  gausslemma2dlem2  15757  gausslemma2dlem3  15758  lgsquadlemofi  15771  lgsquadlem1  15772  lgsquadlem2  15773  2lgslem1a1  15781  2sqlem6  15815  2sqlem8  15818  2sqlem10  15820  usgruspgrben  16000  uspgredg2v  16035  usgredg2v  16038  vtxedgfi  16049  vtxlpfi  16050  wlk1walkdom  16105  wlkres  16123  fnmptd  16251  bj-charfun  16253  bj-charfundc  16254  bj-charfunr  16256  2omap  16446  pw1nct  16456  nnsf  16459  nninfalllem1  16462  nninfall  16463  nninfself  16467  nninfsellemeq  16468  nninfsellemeqinf  16470  nninfsel  16471  nnnninfex  16476  nninfnfiinf  16477  isomninnlem  16486  trilpolemeq1  16496  trilpo  16499  apdiff  16504  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508  redcwlpo  16511  redc0  16513  reap0  16514  dceqnconst  16516  dcapnconst  16517  nconstwlpolem  16521  nconstwlpo  16522  neapmkv  16524  ltlenmkv  16526