Theorem ralrimiva 2579

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2176  ∀wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralrimivvva  2589  rgen2  2592  rgen3  2593  nrexdv  2599  r19.29vva  2651  rabbidva  2760  ssrabdv  3272  ss2rabdv  3274  iuneq2dv  3948  iunssd  3973  disjeq2dv  4026  mpteq12dva  4126  triun  4156  issod  4367  frirrg  4398  frind  4400  peano2  4644  dmmptd  5408  fun11iun  5545  fniinfv  5639  eqfnfv  5679  eqfnfvd  5682  fnmptfvd  5686  dff3im  5727  dffo4  5730  fmptd  5736  ffnfv  5740  fmpt2d  5744  ffvresb  5745  funiun  5763  fconst2g  5801  fconstfvm  5804  resfunexg  5807  eufnfv  5817  foco2  5824  fniunfv  5833  fcofo  5855  fliftel  5864  fliftfun  5867  fliftfuns  5869  riota5f  5926  f1ocnvd  6150  suppssov1  6157  offval2  6176  ofrfval2  6177  offveqb  6180  offveq  6181  caofref  6185  caofinvl  6186  caofid0l  6187  caofid0r  6188  caofid1  6189  caofid2  6190  opabex3d  6208  uchoice  6225  oprssdmm  6259  f1od2  6323  disjxp1  6324  tfrlem1  6396  tfrlemisucaccv  6413  tfrlemiubacc  6418  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemubacc  6434  tfr1onlemaccex  6436  tfr1onlemres  6437  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemubacc  6447  tfrcllemaccex  6449  tfrcllemres  6450  tfrcl  6452  rdgon  6474  freccllem  6490  frecfcllem  6492  omcl  6549  oeicl  6550  qliftfuns  6708  ixpeq2dva  6802  xpf1o  6943  mapxpen  6947  isinfinf  6996  fimax2gtrilemstep  6999  undifdcss  7022  opabfi  7037  eqsuptid  7101  eqinftid  7125  difinfsnlem  7203  difinfsn  7204  ctmlemr  7212  ctm  7213  ctssdclemn0  7214  ctssdccl  7215  enumctlemm  7218  nninfninc  7227  nnnninf  7230  nnnninfeq  7232  enomnilem  7242  ismkvnex  7259  enmkvlem  7265  enwomnilem  7273  nninfwlporlemd  7276  nninfwlpoimlemg  7279  nninfwlpoimlemginf  7280  nninfwlpoim  7283  nninfinfwlpo  7284  finacn  7318  acfun  7321  exmidaclem  7322  exmidontriimlem4  7338  exmidontriim  7339  pw1on  7340  ccfunen  7378  cc2lem  7380  cc3  7382  acnccim  7386  genprndl  7636  genprndu  7637  nqprloc  7660  ltexprlemrnd  7720  ltexprlemdisj  7721  lteupri  7732  recexprlemrnd  7744  recexprlemdisj  7745  caucvgprlemlim  7796  caucvgprprlemlim  7826  suplocexprlemml  7831  suplocexprlemrl  7832  suplocexprlemmu  7833  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemub  7838  caucvgsrlembound  7909  caucvgsrlemgt1  7910  caucvgsrlemoffgt1  7914  caucvgsr  7917  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  elrealeu  7944  axcaucvglemcau  8013  axcaucvglemres  8014  axpre-suploclemres  8016  negeu  8265  eqord1  8558  eqord2  8559  creur  9034  creui  9035  suprzclex  9473  supinfneg  9718  infsupneg  9719  infregelbex  9721  indstr2  9732  iooidg  10033  iccsupr  10090  icoshftf1o  10115  fznlem  10165  exfzdc  10371  zsupcllemstep  10374  infssuzex  10378  suprzubdc  10381  zsupssdc  10383  exbtwnzlemstep  10392  exbtwnzlemex  10394  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgtcl  10559  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgfunlem  10566  frecuzrdgsuctlem  10570  nninfinf  10590  iseqovex  10605  seq3val  10607  seqvalcd  10608  seq3-1  10609  seqf  10611  seq3p1  10612  seqovcd  10614  seqp1cd  10617  seq3clss  10618  seq3fveq2  10622  seqfveq2g  10624  seqfveqg  10625  seq3fveq  10626  seq3feq  10627  seq3shft2  10628  seqshft2g  10629  monoord  10632  monoord2  10633  ser3mono  10634  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seqcaopr3g  10639  seq3caopr2  10640  seqcaopr2g  10641  iseqf1olemqk  10654  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seq3f1oleml  10663  seq3f1o  10664  seqf1og  10668  seq3id3  10671  seq3id  10672  seq3id2  10673  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  ser3ge0  10683  nn0ltexp2  10856  bccl  10914  hashinfuni  10924  hashennnuni  10926  wrdexg  11007  ccatlen  11054  ccatvalfn  11060  ccatrn  11068  swrdlen  11108  swrdwrdsymbg  11120  shftf  11174  seq3shft  11182  caucvgrelemcau  11324  cvg1nlemcau  11328  cvg1nlemres  11329  resqrexlemcvg  11363  resqrexlemglsq  11366  resqrexlemga  11367  maxabslemval  11552  negfi  11572  minmax  11574  xrmaxiflemval  11594  xrminmax  11609  climconst  11634  2clim  11645  climcn1  11652  climcn2  11653  reccn2ap  11657  cn1lem  11658  climsqz  11679  climsqz2  11680  climcau  11691  climrecvg1n  11692  serf0  11696  sumeq2dv  11712  sumrbdclem  11721  fsum3cvg  11722  summodclem3  11724  summodclem2a  11725  zsumdc  11728  isum  11729  fsumgcl  11730  fsum3  11731  fsumf1o  11734  isumss  11735  fisumss  11736  isumss2  11737  fsum3cvg2  11738  fsumsersdc  11739  fsum3ser  11741  fsumcl2lem  11742  fsumadd  11750  fsumsplit  11751  fsumm1  11760  fsum1p  11762  isumclim3  11767  isummulc2  11770  sumsplitdc  11776  fsum2dlemstep  11778  fisumcom2  11782  fsumshftm  11789  fsummulc2  11792  fsumge1  11805  fsum00  11806  fsumabs  11809  telfsumo  11810  telfsumo2  11811  fsumparts  11814  fsumrelem  11815  fsumiun  11821  hashiun  11822  hash2iun  11823  binomlem  11827  isumshft  11834  isum1p  11836  isumnn0nn  11837  isumrpcl  11838  isumlessdc  11840  divcnv  11841  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratnnlemseq  11870  cvgratnnlemabsle  11871  cvgratnnlemfm  11873  cvgratnnlemrate  11874  cvgratnn  11875  cvgratz  11876  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  clim2prod  11883  prodeq2dv  11910  prodrbdclem  11915  fproddccvg  11916  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  iprodap  11924  fprodseq  11927  fprodf1o  11932  prodssdc  11933  fprodssdc  11934  fprodmul  11935  fprodsplit  11941  fprodm1  11942  fprod1p  11943  fprodm1s  11945  fprodp1s  11946  fprodunsn  11948  fprodcl2lem  11949  fprodabs  11960  fprodeq0  11961  fprodap0  11965  fprod2dlemstep  11966  fprodcom2fi  11970  fprodrec  11973  fprodmodd  11985  efcvgfsum  12011  dvdsssfz1  12196  bitsfi  12301  bitsinv1  12306  dvdsbnd  12310  bezoutlemstep  12351  bezoutlemmain  12352  bezoutlemle  12362  bezoutlemsup  12363  dfgcd3  12364  dfgcd2  12368  nnwodc  12390  uzwodc  12391  nnwosdc  12393  nninfctlemfo  12394  coprmgcdb  12443  prmdc  12485  isprm5  12497  isprm6  12502  phivalfi  12567  phibndlem  12571  dfphi2  12575  hashdvds  12576  phiprmpw  12577  phimullem  12580  eulerthlemfi  12583  dvdsfi  12594  hashgcdeq  12595  phisum  12596  reumodprminv  12609  pclemdc  12644  pc2dvds  12686  pcz  12688  pcprmpw2  12689  pcmptdvds  12701  pcprod  12702  pcfac  12706  qexpz  12708  prmpwdvds  12711  pockthg  12713  infpnlem2  12716  1arithlem4  12722  1arith  12723  4sqlemafi  12751  4sqlemffi  12752  4sqleminfi  12753  ennnfonelemex  12818  ennnfonelemfun  12821  ennnfonelemf1  12822  ennnfonelemnn0  12826  ennnfonelemim  12828  exmidunben  12830  ctinfomlemom  12831  ctinfom  12832  ctinf  12834  ctiunctlemudc  12841  ctiunctlemf  12842  ctiunctlemfo  12843  omctfn  12847  ssnnctlemct  12850  nninfdclemcl  12852  nninfdclemp1  12854  pwsbas  13157  imasival  13171  ismgmid2  13245  mgmidsssn0  13249  grpinvalem  13250  grpinva  13251  gsumress  13260  issgrpd  13277  prdsplusgsgrpcl  13279  sgrpidmndm  13285  ismndd  13302  mndpfo  13303  prdsplusgcl  13311  prdsidlem  13312  mhmima  13356  mhmeql  13357  gsumvallem2  13358  isgrpd2e  13385  dfgrp2  13392  grpidd2  13406  isgrpinv  13419  grplrinv  13422  grpidinv  13424  dfgrp3me  13465  prdsinvlem  13473  mhmmnd  13485  ghmgrp  13487  mulgsubcl  13505  issubg2m  13558  issubgrpd2  13559  grpissubg  13563  subgintm  13567  nmzsubg  13579  ssnmz  13580  ghmrn  13626  ghmeql  13636  ghmf1  13642  conjnmz  13648  conjnmzb  13649  rinvmod  13678  srgrz  13779  srglz  13780  srgisid  13781  ringsrg  13842  rhmdvdsr  13970  rhmopp  13971  subrngintm  14007  subrg1  14026  subrgugrp  14035  subrgintm  14038  unitrrg  14062  aprap  14081  islmodd  14088  lssuni  14158  lsssubg  14172  lssintclm  14179  dflidl2rng  14276  lidlsubg  14281  cnsubglem  14374  gsumfzfsumlemm  14382  znf1o  14446  znidomb  14453  psrbagfi  14468  psr1clfi  14483  mplsubgfilemm  14493  mplsubgfilemcl  14494  mplsubgfi  14496  fiinbas  14554  tgclb  14570  restbasg  14673  iscnp4  14723  cnco  14726  cnptopco  14727  cnss1  14731  cnss2  14732  cncnpi  14733  cncnp  14735  cnconst2  14738  cnrest  14740  cnptopresti  14743  cnpdis  14747  lmtopcnp  14755  txbasval  14772  tx1cn  14774  tx2cn  14775  txcnp  14776  upxp  14777  txdis1cn  14783  cnmpt11  14788  psmet0  14832  psmettri2  14833  psmetxrge0  14837  psmetres2  14838  ismeti  14851  xmetpsmet  14874  blsscls2  14998  comet  15004  xmettx  15015  tgioo  15059  tgqioo  15060  fsumcncntop  15072  elcncf1di  15084  cdivcncfap  15109  mulcncflem  15112  mulcncf  15113  cnopnap  15116  divcncfap  15119  dedekindeulemuub  15122  dedekindeulemlu  15126  suplociccreex  15129  suplociccex  15130  dedekindicclemuub  15131  dedekindicclemlu  15135  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemdisj  15145  ivthinclemloc  15146  ivthinc  15148  ivthdec  15149  dich0  15157  ivthdich  15158  cnplimclemr  15174  limccnp2cntop  15182  limccoap  15183  dvcn  15205  dvfre  15215  dvrecap  15218  dvmptclx  15223  dvmptaddx  15224  dvmptmulx  15225  dveflem  15231  dvef  15232  ply1termlem  15247  plyaddlem1  15252  plymullem1  15253  plycoeid3  15262  plycj  15266  plyreres  15269  dvply1  15270  sin0pilem1  15286  sin0pilem2  15287  mpodvdsmulf1o  15495  mersenne  15502  perfectlem2  15505  lgsval2lem  15520  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem1f1o  15570  gausslemma2dlem2  15572  gausslemma2dlem3  15573  lgsquadlemofi  15586  lgsquadlem1  15587  lgsquadlem2  15588  2lgslem1a1  15596  2sqlem6  15630  2sqlem8  15633  2sqlem10  15635  fnmptd  15777  bj-charfun  15780  bj-charfundc  15781  bj-charfunr  15783  2omap  15969  pw1nct  15977  nnsf  15979  nninfalllem1  15982  nninfall  15983  nninfself  15987  nninfsellemeq  15988  nninfsellemeqinf  15990  nninfsel  15991  nnnninfex  15996  nninfnfiinf  15997  isomninnlem  16006  trilpolemeq1  16016  trilpo  16019  apdiff  16024  iswomninnlem  16025  iswomni0  16027  ismkvnnlem  16028  redcwlpo  16031  redc0  16033  reap0  16034  dceqnconst  16036  dcapnconst  16037  nconstwlpolem  16041  nconstwlpo  16042  neapmkv  16044  ltlenmkv  16046