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  3321  ss2rabdv  3323  iuneq2dv  4017  iunssd  4042  disjeq2dv  4095  mpteq12dva  4196  triun  4226  issod  4445  frirrg  4476  frind  4478  peano2  4722  dmmptd  5494  fun11iun  5640  fniinfv  5740  eqfnfv  5780  eqfnfvd  5783  fnmptfvd  5787  dff3im  5827  dffo4  5830  fmptd  5836  ffnfv  5840  fmpt2d  5844  ffvresb  5845  funiun  5864  fconst2g  5904  fconstfvm  5907  resfunexg  5910  eufnfv  5922  foco2  5932  fniunfv  5941  fcofo  5963  fliftel  5972  fliftfun  5975  fliftfuns  5977  riota5f  6038  f1ocnvd  6265  f1o3d  6271  suppssov1  6272  offval2  6291  ofrfval2  6292  offveqb  6295  offveq  6296  caofref  6300  caofinvl  6301  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  opabex3d  6323  uchoice  6344  oprssdmm  6378  f1od2  6444  disjxp1  6445  funsssuppss  6471  suppofss1dcl  6477  suppofss2dcl  6478  tfrlem1  6552  tfrlemisucaccv  6569  tfrlemiubacc  6574  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemubacc  6590  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemubacc  6603  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  rdgon  6630  freccllem  6646  frecfcllem  6648  omcl  6707  oeicl  6708  qliftfuns  6866  ixpeq2dva  6961  xpf1o  7110  mapxpen  7114  isinfinf  7167  fimax2gtrilemstep  7171  undifdcss  7196  opabfi  7213  fissfi  7229  2omap  7282  eqsuptid  7301  eqinftid  7325  difinfsnlem  7403  difinfsn  7404  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  enumctlemm  7418  nninfninc  7427  nnnninf  7430  nnnninfeq  7432  enomnilem  7442  ismkvnex  7459  enmkvlem  7465  enwomnilem  7473  nninfwlporlemd  7476  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  nninfwlpoim  7483  nninfinfwlpo  7484  finacn  7524  acfun  7527  exmidaclem  7528  exmidontriimlem4  7544  exmidontriim  7545  pw1on  7549  ccfunen  7594  cc2lem  7596  cc3  7598  acnccim  7602  genprndl  7852  genprndu  7853  nqprloc  7876  ltexprlemrnd  7936  ltexprlemdisj  7937  lteupri  7948  recexprlemrnd  7960  recexprlemdisj  7961  caucvgprlemlim  8012  caucvgprprlemlim  8042  suplocexprlemml  8047  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  caucvgsrlembound  8125  caucvgsrlemgt1  8126  caucvgsrlemoffgt1  8130  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  elrealeu  8160  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  negeu  8480  eqord1  8774  eqord2  8775  creur  9250  creui  9251  suprzclex  9694  supinfneg  9945  infsupneg  9946  infregelbex  9948  indstr2  9959  iooidg  10261  iccsupr  10318  icoshftf1o  10343  fznlem  10395  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  suprzubdc  10620  zsupssdc  10622  exbtwnzlemstep  10631  exbtwnzlemex  10633  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgtcl  10798  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgfunlem  10805  frecuzrdgsuctlem  10809  nninfinf  10829  iseqovex  10844  seq3val  10846  seqvalcd  10847  seq3-1  10848  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3clss  10857  seq3fveq2  10861  seqfveq2g  10863  seqfveqg  10864  seq3fveq  10865  seq3feq  10866  seq3shft2  10867  seqshft2g  10868  monoord  10871  monoord2  10872  ser3mono  10873  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemqk  10893  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  seqf1og  10907  seq3id3  10910  seq3id  10911  seq3id2  10912  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  ser3ge0  10922  nn0ltexp2  11096  bccl  11154  hashinfuni  11165  hashennnuni  11167  sshashneg  11230  hashfibclem  11231  wrdexg  11260  ccatlen  11308  ccatvalfn  11314  ccatrn  11322  swrdlen  11369  swrdwrdsymbg  11381  swrdswrd  11422  wrdind  11439  reuccatpfxs1  11464  shftf  11540  seq3shft  11548  caucvgrelemcau  11690  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemcvg  11729  resqrexlemglsq  11732  resqrexlemga  11733  maxabslemval  11918  negfi  11938  minmax  11940  xrmaxiflemval  11960  xrminmax  11975  climconst  12000  2clim  12011  climcn1  12018  climcn2  12019  reccn2ap  12023  cn1lem  12024  climsqz  12045  climsqz2  12046  climcau  12057  climrecvg1n  12058  serf0  12062  sumeq2dv  12078  sumrbdclem  12088  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  zsumdc  12095  isum  12096  fsumgcl  12097  fsum3  12098  fsumf1o  12101  isumss  12102  fisumss  12103  isumss2  12104  fsum3cvg2  12105  fsumsersdc  12106  fsum3ser  12108  fsumcl2lem  12109  fsumadd  12117  fsumsplit  12118  fsumm1  12127  fsum1p  12129  isumclim3  12134  isummulc2  12137  sumsplitdc  12143  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fsummulc2  12159  fsumge1  12172  fsum00  12173  fsumabs  12176  telfsumo  12177  telfsumo2  12178  fsumparts  12181  fsumrelem  12182  fsumiun  12188  hashiun  12189  hash2iun  12190  binomlem  12194  isumshft  12201  isum1p  12203  isumnn0nn  12204  isumrpcl  12205  isumlessdc  12207  divcnv  12208  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratnn  12242  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2prod  12250  prodeq2dv  12277  prodrbdclem  12282  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  iprodap  12291  fprodseq  12294  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  fprodsplit  12308  fprodm1  12309  fprod1p  12310  fprodm1s  12312  fprodp1s  12313  fprodunsn  12315  fprodcl2lem  12316  fprodabs  12327  fprodeq0  12328  fprodap0  12332  fprod2dlemstep  12333  fprodcom2fi  12337  fprodrec  12340  fprodmodd  12352  efcvgfsum  12378  dvdsssfz1  12563  bitsfi  12668  bitsinv1  12673  dvdsbnd  12677  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemle  12729  bezoutlemsup  12730  dfgcd3  12731  dfgcd2  12735  nnwodc  12757  uzwodc  12758  nnwosdc  12760  nninfctlemfo  12761  coprmgcdb  12810  prmdc  12852  isprm5  12864  isprm6  12869  phivalfi  12934  phibndlem  12938  dfphi2  12942  hashdvds  12943  phiprmpw  12944  phimullem  12947  eulerthlemfi  12950  dvdsfi  12961  hashgcdeq  12962  phisum  12963  reumodprminv  12976  pclemdc  13011  pc2dvds  13053  pcz  13055  pcprmpw2  13056  pcmptdvds  13068  pcprod  13069  pcfac  13073  qexpz  13075  prmpwdvds  13078  pockthg  13080  infpnlem2  13083  1arithlem4  13089  1arith  13090  4sqlemafi  13118  4sqlemffi  13119  4sqleminfi  13120  ballotfilemcinfi  13168  ballotfilemdifcfi  13169  ballotfilemcinfz  13170  ballotfilemdifcfz  13171  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilemiex  13188  ennnfonelemex  13249  ennnfonelemfun  13252  ennnfonelemf1  13253  ennnfonelemnn0  13257  ennnfonelemim  13259  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctinf  13265  ctiunctlemudc  13272  ctiunctlemf  13273  ctiunctlemfo  13274  omctfn  13278  ssnnctlemct  13281  nninfdclemcl  13283  nninfdclemp1  13285  imasival  13570  ismgmid2  13643  mgmidsssn0  13647  grpinvalem  13648  grpinva  13649  gsumress  13658  issgrpd  13675  sgrpidmndm  13681  ismndd  13698  mndpfo  13699  mhmima  13746  mhmeql  13747  gsumvallem2  13748  isgrpd2e  13775  dfgrp2  13782  grpidd2  13796  isgrpinv  13809  grplrinv  13812  grpidinv  13814  dfgrp3me  13855  mhmmnd  13869  ghmgrp  13871  mulgsubcl  13889  issubg2m  13942  issubgrpd2  13943  grpissubg  13947  subgintm  13951  nmzsubg  13963  ssnmz  13964  ghmrn  14010  ghmeql  14020  ghmf1  14026  conjnmz  14032  conjnmzb  14033  rinvmod  14062  prdsplusgsgrpcl  14132  prdsplusgcl  14134  prdsidlem  14135  prdsinvlem  14138  pwsbas  14147  srgrz  14227  srglz  14228  srgisid  14229  ringsrg  14290  rhmdvdsr  14420  rhmopp  14421  subrngintm  14458  subrg1  14477  subrgugrp  14486  subrgintm  14489  rrgsupp  14512  unitrrg  14514  aprap  14536  islmodd  14567  lssuni  14637  lsssubg  14651  lssintclm  14658  dflidl2rng  14755  lidlsubg  14760  cnsubglem  14853  gsumfzfsumlemm  14861  znf1o  14925  znidomb  14932  psrbagfi  14949  psrbaglecl  14950  psrbagcon  14952  psr1clfi  14969  mplsubgfilemm  14979  mplsubgfilemcl  14980  mplsubgfi  14982  fiinbas  15040  tgclb  15056  restbasg  15159  iscnp4  15209  cnco  15212  cnptopco  15213  cnss1  15217  cnss2  15218  cncnpi  15219  cncnp  15221  cnconst2  15224  cnrest  15226  cnptopresti  15229  cnpdis  15233  lmtopcnp  15241  txbasval  15258  tx1cn  15260  tx2cn  15261  txcnp  15262  upxp  15263  txdis1cn  15269  cnmpt11  15274  psmet0  15318  psmettri2  15319  psmetxrge0  15323  psmetres2  15324  ismeti  15337  xmetpsmet  15360  blsscls2  15484  comet  15490  xmettx  15501  tgioo  15545  tgqioo  15546  fsumcncntop  15558  elcncf1di  15570  cdivcncfap  15595  mulcncflem  15598  mulcncf  15599  cnopnap  15602  divcncfap  15605  dedekindeulemuub  15608  dedekindeulemlu  15612  suplociccreex  15615  suplociccex  15616  dedekindicclemuub  15617  dedekindicclemlu  15621  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemdisj  15631  ivthinclemloc  15632  ivthinc  15634  ivthdec  15635  dich0  15643  ivthdich  15644  cnplimclemr  15660  limccnp2cntop  15668  limccoap  15669  dvcn  15691  dvfre  15701  dvrecap  15704  dvmptclx  15709  dvmptaddx  15710  dvmptmulx  15711  dveflem  15717  dvef  15718  ply1termlem  15733  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  plycj  15752  plyreres  15755  dvply1  15756  sin0pilem1  15772  sin0pilem2  15773  mpodvdsmulf1o  15984  mersenne  15991  perfectlem2  15994  lgsval2lem  16009  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1f1o  16059  gausslemma2dlem2  16061  gausslemma2dlem3  16062  lgsquadlemofi  16075  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1a1  16085  2sqlem6  16119  2sqlem8  16122  2sqlem10  16124  usgruspgrben  16307  uspgredg2v  16342  usgredg2v  16345  subuhgr  16393  subupgr  16394  subumgr  16395  subusgr  16396  vtxedgfi  16410  vtxlpfi  16411  wlk1walkdom  16480  wlkres  16500  eupth2lembfi  16598  depindlem1  16627  depindlem2  16628  depindlem3  16629  fnmptd  16702  bj-charfun  16703  bj-charfundc  16704  bj-charfunr  16706  pw1nct  16903  nnsf  16909  nninfalllem1  16912  nninfall  16913  nninfself  16917  nninfsellemeq  16918  nninfsellemeqinf  16920  nninfsel  16921  nnnninfex  16926  nninfnfiinf  16927  repiecef  16938  isomninnlem  16940  trilpolemeq1  16950  trilpo  16953  apdiff  16958  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963  redcwlpo  16966  redc0  16968  reap0  16969  trimul0or  16971  dceqnconst  16972  dcapnconst  16973  nconstwlpolem  16977  nconstwlpo  16978  neapmkv  16980  ltlenmkv  16982