Theorem ralrimiva 2617

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∀wral 2522

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 2527

This theorem is referenced by:  ralrimivvva  2627  rgen2  2630  rgen3  2631  nrexdv  2637  r19.29vva  2690  rabbidva  2803  ssrabdv  3319  ss2rabdv  3321  iuneq2dv  4014  iunssd  4039  disjeq2dv  4092  mpteq12dva  4193  triun  4223  issod  4442  frirrg  4473  frind  4475  peano2  4719  dmmptd  5491  fun11iun  5637  fniinfv  5737  eqfnfv  5777  eqfnfvd  5780  fnmptfvd  5784  dff3im  5824  dffo4  5827  fmptd  5833  ffnfv  5837  fmpt2d  5841  ffvresb  5842  funiun  5861  fconst2g  5901  fconstfvm  5904  resfunexg  5907  eufnfv  5919  foco2  5928  fniunfv  5937  fcofo  5959  fliftel  5968  fliftfun  5971  fliftfuns  5973  riota5f  6032  f1ocnvd  6259  suppssov1  6265  offval2  6284  ofrfval2  6285  offveqb  6288  offveq  6289  caofref  6293  caofinvl  6294  caofid0l  6295  caofid0r  6296  caofid1  6297  caofid2  6298  opabex3d  6316  uchoice  6333  oprssdmm  6367  f1od2  6433  disjxp1  6434  funsssuppss  6460  suppofss1dcl  6466  suppofss2dcl  6467  tfrlem1  6541  tfrlemisucaccv  6558  tfrlemiubacc  6563  tfr1onlemsucfn  6573  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemubacc  6579  tfr1onlemaccex  6581  tfr1onlemres  6582  tfrcllemsucfn  6586  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemubacc  6592  tfrcllemaccex  6594  tfrcllemres  6595  tfrcl  6597  rdgon  6619  freccllem  6635  frecfcllem  6637  omcl  6696  oeicl  6697  qliftfuns  6855  ixpeq2dva  6950  xpf1o  7099  mapxpen  7103  isinfinf  7156  fimax2gtrilemstep  7160  undifdcss  7185  opabfi  7202  fissfi  7218  2omap  7271  eqsuptid  7290  eqinftid  7314  difinfsnlem  7392  difinfsn  7393  ctmlemr  7401  ctm  7402  ctssdclemn0  7403  ctssdccl  7404  enumctlemm  7407  nninfninc  7416  nnnninf  7419  nnnninfeq  7421  enomnilem  7431  ismkvnex  7448  enmkvlem  7454  enwomnilem  7462  nninfwlporlemd  7465  nninfwlpoimlemg  7468  nninfwlpoimlemginf  7469  nninfwlpoim  7472  nninfinfwlpo  7473  finacn  7513  acfun  7516  exmidaclem  7517  exmidontriimlem4  7533  exmidontriim  7534  pw1on  7538  ccfunen  7580  cc2lem  7582  cc3  7584  acnccim  7588  genprndl  7838  genprndu  7839  nqprloc  7862  ltexprlemrnd  7922  ltexprlemdisj  7923  lteupri  7934  recexprlemrnd  7946  recexprlemdisj  7947  caucvgprlemlim  7998  caucvgprprlemlim  8028  suplocexprlemml  8033  suplocexprlemrl  8034  suplocexprlemmu  8035  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemloc  8038  suplocexprlemub  8040  caucvgsrlembound  8111  caucvgsrlemgt1  8112  caucvgsrlemoffgt1  8116  caucvgsr  8119  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  elrealeu  8146  axcaucvglemcau  8215  axcaucvglemres  8216  axpre-suploclemres  8218  negeu  8466  eqord1  8759  eqord2  8760  creur  9235  creui  9236  suprzclex  9679  supinfneg  9930  infsupneg  9931  infregelbex  9933  indstr2  9944  iooidg  10245  iccsupr  10302  icoshftf1o  10327  fznlem  10378  exfzdc  10590  zsupcllemstep  10593  infssuzex  10597  suprzubdc  10600  zsupssdc  10602  exbtwnzlemstep  10611  exbtwnzlemex  10613  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgtcl  10778  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgfunlem  10785  frecuzrdgsuctlem  10789  nninfinf  10809  iseqovex  10824  seq3val  10826  seqvalcd  10827  seq3-1  10828  seqf  10830  seq3p1  10831  seqovcd  10833  seqp1cd  10836  seq3clss  10837  seq3fveq2  10841  seqfveq2g  10843  seqfveqg  10844  seq3fveq  10845  seq3feq  10846  seq3shft2  10847  seqshft2g  10848  monoord  10851  monoord2  10852  ser3mono  10853  seq3split  10854  seqsplitg  10855  seq3caopr3  10857  seqcaopr3g  10858  seq3caopr2  10859  seqcaopr2g  10860  iseqf1olemqk  10873  iseqf1olemjpcl  10874  iseqf1olemqpcl  10875  iseqf1olemfvp  10876  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seq3f1olemqsum  10879  seq3f1oleml  10882  seq3f1o  10883  seqf1og  10887  seq3id3  10890  seq3id  10891  seq3id2  10892  seq3homo  10893  seq3z  10894  seqhomog  10896  seqfeq4g  10897  ser3ge0  10902  nn0ltexp2  11075  bccl  11133  hashinfuni  11144  hashennnuni  11146  sshashneg  11209  hashfibclem  11210  wrdexg  11239  ccatlen  11287  ccatvalfn  11293  ccatrn  11301  swrdlen  11348  swrdwrdsymbg  11360  swrdswrd  11401  wrdind  11418  reuccatpfxs1  11443  shftf  11519  seq3shft  11527  caucvgrelemcau  11669  cvg1nlemcau  11673  cvg1nlemres  11674  resqrexlemcvg  11708  resqrexlemglsq  11711  resqrexlemga  11712  maxabslemval  11897  negfi  11917  minmax  11919  xrmaxiflemval  11939  xrminmax  11954  climconst  11979  2clim  11990  climcn1  11997  climcn2  11998  reccn2ap  12002  cn1lem  12003  climsqz  12024  climsqz2  12025  climcau  12036  climrecvg1n  12037  serf0  12041  sumeq2dv  12057  sumrbdclem  12067  fsum3cvg  12068  summodclem3  12070  summodclem2a  12071  zsumdc  12074  isum  12075  fsumgcl  12076  fsum3  12077  fsumf1o  12080  isumss  12081  fisumss  12082  isumss2  12083  fsum3cvg2  12084  fsumsersdc  12085  fsum3ser  12087  fsumcl2lem  12088  fsumadd  12096  fsumsplit  12097  fsumm1  12106  fsum1p  12108  isumclim3  12113  isummulc2  12116  sumsplitdc  12122  fsum2dlemstep  12124  fisumcom2  12128  fsumshftm  12135  fsummulc2  12138  fsumge1  12151  fsum00  12152  fsumabs  12155  telfsumo  12156  telfsumo2  12157  fsumparts  12160  fsumrelem  12161  fsumiun  12167  hashiun  12168  hash2iun  12169  binomlem  12173  isumshft  12180  isum1p  12182  isumnn0nn  12183  isumrpcl  12184  isumlessdc  12186  divcnv  12187  cvgratnnlemnexp  12214  cvgratnnlemmn  12215  cvgratnnlemseq  12216  cvgratnnlemabsle  12217  cvgratnnlemfm  12219  cvgratnnlemrate  12220  cvgratnn  12221  cvgratz  12222  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  clim2prod  12229  prodeq2dv  12256  prodrbdclem  12261  fproddccvg  12262  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  iprodap  12270  fprodseq  12273  fprodf1o  12278  prodssdc  12279  fprodssdc  12280  fprodmul  12281  fprodsplit  12287  fprodm1  12288  fprod1p  12289  fprodm1s  12291  fprodp1s  12292  fprodunsn  12294  fprodcl2lem  12295  fprodabs  12306  fprodeq0  12307  fprodap0  12311  fprod2dlemstep  12312  fprodcom2fi  12316  fprodrec  12319  fprodmodd  12331  efcvgfsum  12357  dvdsssfz1  12542  bitsfi  12647  bitsinv1  12652  dvdsbnd  12656  bezoutlemstep  12697  bezoutlemmain  12698  bezoutlemle  12708  bezoutlemsup  12709  dfgcd3  12710  dfgcd2  12714  nnwodc  12736  uzwodc  12737  nnwosdc  12739  nninfctlemfo  12740  coprmgcdb  12789  prmdc  12831  isprm5  12843  isprm6  12848  phivalfi  12913  phibndlem  12917  dfphi2  12921  hashdvds  12922  phiprmpw  12923  phimullem  12926  eulerthlemfi  12929  dvdsfi  12940  hashgcdeq  12941  phisum  12942  reumodprminv  12955  pclemdc  12990  pc2dvds  13032  pcz  13034  pcprmpw2  13035  pcmptdvds  13047  pcprod  13048  pcfac  13052  qexpz  13054  prmpwdvds  13057  pockthg  13059  infpnlem2  13062  1arithlem4  13068  1arith  13069  4sqlemafi  13097  4sqlemffi  13098  4sqleminfi  13099  ballotfilemcinfi  13147  ballotfilemdifcfi  13148  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemodife  13158  ennnfonelemex  13182  ennnfonelemfun  13185  ennnfonelemf1  13186  ennnfonelemnn0  13190  ennnfonelemim  13192  exmidunben  13194  ctinfomlemom  13195  ctinfom  13196  ctinf  13198  ctiunctlemudc  13205  ctiunctlemf  13206  ctiunctlemfo  13207  omctfn  13211  ssnnctlemct  13214  nninfdclemcl  13216  nninfdclemp1  13218  pwsbas  13522  imasival  13536  ismgmid2  13610  mgmidsssn0  13614  grpinvalem  13615  grpinva  13616  gsumress  13625  issgrpd  13642  prdsplusgsgrpcl  13644  sgrpidmndm  13650  ismndd  13667  mndpfo  13668  prdsplusgcl  13676  prdsidlem  13677  mhmima  13721  mhmeql  13722  gsumvallem2  13723  isgrpd2e  13750  dfgrp2  13757  grpidd2  13771  isgrpinv  13784  grplrinv  13787  grpidinv  13789  dfgrp3me  13830  prdsinvlem  13838  mhmmnd  13850  ghmgrp  13852  mulgsubcl  13870  issubg2m  13923  issubgrpd2  13924  grpissubg  13928  subgintm  13932  nmzsubg  13944  ssnmz  13945  ghmrn  13991  ghmeql  14001  ghmf1  14007  conjnmz  14013  conjnmzb  14014  rinvmod  14043  srgrz  14145  srglz  14146  srgisid  14147  ringsrg  14208  rhmdvdsr  14337  rhmopp  14338  subrngintm  14374  subrg1  14393  subrgugrp  14402  subrgintm  14405  rrgsupp  14428  unitrrg  14430  aprap  14449  islmodd  14458  lssuni  14528  lsssubg  14542  lssintclm  14549  dflidl2rng  14646  lidlsubg  14651  cnsubglem  14744  gsumfzfsumlemm  14752  znf1o  14816  znidomb  14823  psrbagfi  14840  psrbaglecl  14841  psrbagcon  14843  psr1clfi  14860  mplsubgfilemm  14870  mplsubgfilemcl  14871  mplsubgfi  14873  fiinbas  14931  tgclb  14947  restbasg  15050  iscnp4  15100  cnco  15103  cnptopco  15104  cnss1  15108  cnss2  15109  cncnpi  15110  cncnp  15112  cnconst2  15115  cnrest  15117  cnptopresti  15120  cnpdis  15124  lmtopcnp  15132  txbasval  15149  tx1cn  15151  tx2cn  15152  txcnp  15153  upxp  15154  txdis1cn  15160  cnmpt11  15165  psmet0  15209  psmettri2  15210  psmetxrge0  15214  psmetres2  15215  ismeti  15228  xmetpsmet  15251  blsscls2  15375  comet  15381  xmettx  15392  tgioo  15436  tgqioo  15437  fsumcncntop  15449  elcncf1di  15461  cdivcncfap  15486  mulcncflem  15489  mulcncf  15490  cnopnap  15493  divcncfap  15496  dedekindeulemuub  15499  dedekindeulemlu  15503  suplociccreex  15506  suplociccex  15507  dedekindicclemuub  15508  dedekindicclemlu  15512  ivthinclemlopn  15518  ivthinclemlr  15519  ivthinclemuopn  15520  ivthinclemur  15521  ivthinclemdisj  15522  ivthinclemloc  15523  ivthinc  15525  ivthdec  15526  dich0  15534  ivthdich  15535  cnplimclemr  15551  limccnp2cntop  15559  limccoap  15560  dvcn  15582  dvfre  15592  dvrecap  15595  dvmptclx  15600  dvmptaddx  15601  dvmptmulx  15602  dveflem  15608  dvef  15609  ply1termlem  15624  plyaddlem1  15629  plymullem1  15630  plycoeid3  15639  plycj  15643  plyreres  15646  dvply1  15647  sin0pilem1  15663  sin0pilem2  15664  mpodvdsmulf1o  15875  mersenne  15882  perfectlem2  15885  lgsval2lem  15900  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem1f1o  15950  gausslemma2dlem2  15952  gausslemma2dlem3  15953  lgsquadlemofi  15966  lgsquadlem1  15967  lgsquadlem2  15968  2lgslem1a1  15976  2sqlem6  16010  2sqlem8  16013  2sqlem10  16015  usgruspgrben  16198  uspgredg2v  16233  usgredg2v  16236  subuhgr  16284  subupgr  16285  subumgr  16286  subusgr  16287  vtxedgfi  16301  vtxlpfi  16302  wlk1walkdom  16371  wlkres  16391  eupth2lembfi  16489  depindlem1  16518  depindlem2  16519  depindlem3  16520  fnmptd  16593  bj-charfun  16594  bj-charfundc  16595  bj-charfunr  16597  pw1nct  16794  nnsf  16800  nninfalllem1  16803  nninfall  16804  nninfself  16808  nninfsellemeq  16809  nninfsellemeqinf  16811  nninfsel  16812  nnnninfex  16817  nninfnfiinf  16818  repiecef  16829  isomninnlem  16831  trilpolemeq1  16841  trilpo  16844  apdiff  16849  iswomninnlem  16851  iswomni0  16853  ismkvnnlem  16854  redcwlpo  16857  redc0  16859  reap0  16860  trimul0or  16862  dceqnconst  16863  dcapnconst  16864  nconstwlpolem  16868  nconstwlpo  16869  neapmkv  16871  ltlenmkv  16873