Theorem ralrimiva 2567

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  ∀wral 2472

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralrimivvva  2577  rgen2  2580  rgen3  2581  nrexdv  2587  r19.29vva  2639  rabbidva  2748  ssrabdv  3259  ss2rabdv  3261  iuneq2dv  3934  iunssd  3959  disjeq2dv  4012  mpteq12dva  4111  triun  4141  issod  4351  frirrg  4382  frind  4384  peano2  4628  dmmptd  5385  fun11iun  5522  fniinfv  5616  eqfnfv  5656  eqfnfvd  5659  fnmptfvd  5663  dff3im  5704  dffo4  5707  fmptd  5713  ffnfv  5717  fmpt2d  5721  ffvresb  5722  fconst2g  5774  fconstfvm  5777  resfunexg  5780  eufnfv  5790  foco2  5797  fniunfv  5806  fcofo  5828  fliftel  5837  fliftfun  5840  fliftfuns  5842  riota5f  5899  f1ocnvd  6122  suppssov1  6129  offval2  6148  ofrfval2  6149  offveqb  6152  caofref  6156  caofinvl  6157  opabex3d  6175  uchoice  6192  oprssdmm  6226  f1od2  6290  disjxp1  6291  tfrlem1  6363  tfrlemisucaccv  6380  tfrlemiubacc  6385  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemubacc  6401  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemubacc  6414  tfrcllemaccex  6416  tfrcllemres  6417  tfrcl  6419  rdgon  6441  freccllem  6457  frecfcllem  6459  omcl  6516  oeicl  6517  qliftfuns  6675  ixpeq2dva  6769  xpf1o  6902  mapxpen  6906  isinfinf  6955  fimax2gtrilemstep  6958  undifdcss  6981  opabfi  6994  eqsuptid  7058  eqinftid  7082  difinfsnlem  7160  difinfsn  7161  ctmlemr  7169  ctm  7170  ctssdclemn0  7171  ctssdccl  7172  enumctlemm  7175  nninfninc  7184  nnnninf  7187  nnnninfeq  7189  enomnilem  7199  ismkvnex  7216  enmkvlem  7222  enwomnilem  7230  nninfwlporlemd  7233  nninfwlpoimlemg  7236  nninfwlpoimlemginf  7237  nninfwlpoim  7239  acfun  7269  exmidaclem  7270  exmidontriimlem4  7286  exmidontriim  7287  pw1on  7288  ccfunen  7326  cc2lem  7328  cc3  7330  genprndl  7583  genprndu  7584  nqprloc  7607  ltexprlemrnd  7667  ltexprlemdisj  7668  lteupri  7679  recexprlemrnd  7691  recexprlemdisj  7692  caucvgprlemlim  7743  caucvgprprlemlim  7773  suplocexprlemml  7778  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  caucvgsrlembound  7856  caucvgsrlemgt1  7857  caucvgsrlemoffgt1  7861  caucvgsr  7864  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  elrealeu  7891  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  negeu  8212  eqord1  8504  eqord2  8505  creur  8980  creui  8981  suprzclex  9418  supinfneg  9663  infsupneg  9664  infregelbex  9666  indstr2  9677  iooidg  9978  iccsupr  10035  icoshftf1o  10060  fznlem  10110  exfzdc  10310  exbtwnzlemstep  10319  exbtwnzlemex  10321  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgtcl  10486  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgfunlem  10493  frecuzrdgsuctlem  10497  nninfinf  10517  iseqovex  10532  seq3val  10534  seqvalcd  10535  seq3-1  10536  seqf  10538  seq3p1  10539  seqovcd  10541  seqp1cd  10544  seq3clss  10545  seq3fveq2  10549  seqfveq2g  10551  seqfveqg  10552  seq3fveq  10553  seq3feq  10554  seq3shft2  10555  seqshft2g  10556  monoord  10559  monoord2  10560  ser3mono  10561  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemqk  10581  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1oleml  10590  seq3f1o  10591  seqf1og  10595  seq3id3  10598  seq3id  10599  seq3id2  10600  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  ser3ge0  10610  nn0ltexp2  10783  bccl  10841  hashinfuni  10851  hashennnuni  10853  wrdexg  10928  shftf  10977  seq3shft  10985  caucvgrelemcau  11127  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemcvg  11166  resqrexlemglsq  11169  resqrexlemga  11170  maxabslemval  11355  negfi  11374  minmax  11376  xrmaxiflemval  11396  xrminmax  11411  climconst  11436  2clim  11447  climcn1  11454  climcn2  11455  reccn2ap  11459  cn1lem  11460  climsqz  11481  climsqz2  11482  climcau  11493  climrecvg1n  11494  serf0  11498  sumeq2dv  11514  sumrbdclem  11523  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  zsumdc  11530  isum  11531  fsumgcl  11532  fsum3  11533  fsumf1o  11536  isumss  11537  fisumss  11538  isumss2  11539  fsum3cvg2  11540  fsumsersdc  11541  fsum3ser  11543  fsumcl2lem  11544  fsumadd  11552  fsumsplit  11553  fsumm1  11562  fsum1p  11564  isumclim3  11569  isummulc2  11572  sumsplitdc  11578  fsum2dlemstep  11580  fisumcom2  11584  fsumshftm  11591  fsummulc2  11594  fsumge1  11607  fsum00  11608  fsumabs  11611  telfsumo  11612  telfsumo2  11613  fsumparts  11616  fsumrelem  11617  fsumiun  11623  hashiun  11624  hash2iun  11625  binomlem  11629  isumshft  11636  isum1p  11638  isumnn0nn  11639  isumrpcl  11640  isumlessdc  11642  divcnv  11643  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemseq  11672  cvgratnnlemabsle  11673  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratnn  11677  cvgratz  11678  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  clim2prod  11685  prodeq2dv  11712  prodrbdclem  11717  fproddccvg  11718  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  iprodap  11726  fprodseq  11729  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodmul  11737  fprodsplit  11743  fprodm1  11744  fprod1p  11745  fprodm1s  11747  fprodp1s  11748  fprodunsn  11750  fprodcl2lem  11751  fprodabs  11762  fprodeq0  11763  fprodap0  11767  fprod2dlemstep  11768  fprodcom2fi  11772  fprodrec  11775  fprodmodd  11787  efcvgfsum  11813  dvdsssfz1  11997  zsupcllemstep  12085  infssuzex  12089  suprzubdc  12092  zsupssdc  12094  dvdsbnd  12096  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemle  12148  bezoutlemsup  12149  dfgcd3  12150  dfgcd2  12154  nnwodc  12176  uzwodc  12177  nnwosdc  12179  nninfctlemfo  12180  coprmgcdb  12229  prmdc  12271  isprm5  12283  isprm6  12288  phivalfi  12353  phibndlem  12357  dfphi2  12361  hashdvds  12362  phiprmpw  12363  phimullem  12366  eulerthlemfi  12369  hashgcdeq  12380  phisum  12381  reumodprminv  12394  pclemdc  12429  pc2dvds  12471  pcz  12473  pcprmpw2  12474  pcmptdvds  12486  pcprod  12487  pcfac  12491  qexpz  12493  prmpwdvds  12496  pockthg  12498  infpnlem2  12501  1arithlem4  12507  1arith  12508  4sqlemafi  12536  4sqlemffi  12537  4sqleminfi  12538  ennnfonelemex  12574  ennnfonelemfun  12577  ennnfonelemf1  12578  ennnfonelemnn0  12582  ennnfonelemim  12584  exmidunben  12586  ctinfomlemom  12587  ctinfom  12588  ctinf  12590  ctiunctlemudc  12597  ctiunctlemf  12598  ctiunctlemfo  12599  omctfn  12603  ssnnctlemct  12606  nninfdclemcl  12608  nninfdclemp1  12610  imasival  12892  ismgmid2  12966  mgmidsssn0  12970  grpinvalem  12971  grpinva  12972  gsumress  12981  issgrpd  12998  sgrpidmndm  13004  ismndd  13021  mndpfo  13022  mhmima  13066  mhmeql  13067  gsumvallem2  13068  isgrpd2e  13095  dfgrp2  13102  grpidd2  13116  isgrpinv  13129  grplrinv  13132  grpidinv  13134  dfgrp3me  13175  mhmmnd  13189  ghmgrp  13191  mulgsubcl  13209  issubg2m  13262  issubgrpd2  13263  grpissubg  13267  subgintm  13271  nmzsubg  13283  ssnmz  13284  ghmrn  13330  ghmeql  13340  ghmf1  13346  conjnmz  13352  conjnmzb  13353  rinvmod  13382  srgrz  13483  srglz  13484  srgisid  13485  ringsrg  13546  rhmdvdsr  13674  rhmopp  13675  subrngintm  13711  subrg1  13730  subrgugrp  13739  subrgintm  13742  unitrrg  13766  aprap  13785  islmodd  13792  lssuni  13862  lsssubg  13876  lssintclm  13883  dflidl2rng  13980  lidlsubg  13985  cnsubglem  14078  gsumfzfsumlemm  14086  znf1o  14150  znidomb  14157  fiinbas  14228  tgclb  14244  restbasg  14347  iscnp4  14397  cnco  14400  cnptopco  14401  cnss1  14405  cnss2  14406  cncnpi  14407  cncnp  14409  cnconst2  14412  cnrest  14414  cnptopresti  14417  cnpdis  14421  lmtopcnp  14429  txbasval  14446  tx1cn  14448  tx2cn  14449  txcnp  14450  upxp  14451  txdis1cn  14457  cnmpt11  14462  psmet0  14506  psmettri2  14507  psmetxrge0  14511  psmetres2  14512  ismeti  14525  xmetpsmet  14548  blsscls2  14672  comet  14678  xmettx  14689  tgioo  14733  tgqioo  14734  fsumcncntop  14746  elcncf1di  14758  cdivcncfap  14783  mulcncflem  14786  mulcncf  14787  cnopnap  14790  divcncfap  14793  dedekindeulemuub  14796  dedekindeulemlu  14800  suplociccreex  14803  suplociccex  14804  dedekindicclemuub  14805  dedekindicclemlu  14809  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemdisj  14819  ivthinclemloc  14820  ivthinc  14822  ivthdec  14823  dich0  14831  ivthdich  14832  cnplimclemr  14848  limccnp2cntop  14856  limccoap  14857  dvcn  14879  dvfre  14889  dvrecap  14892  dvmptclx  14897  dvmptaddx  14898  dvmptmulx  14899  dveflem  14905  dvef  14906  ply1termlem  14921  plyaddlem1  14926  plymullem1  14927  plycj  14939  plyreres  14942  dvply1  14943  sin0pilem1  14957  sin0pilem2  14958  lgsval2lem  15167  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1f1o  15217  gausslemma2dlem2  15219  gausslemma2dlem3  15220  lgsquadlemofi  15233  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1a1  15243  2sqlem6  15277  2sqlem8  15280  2sqlem10  15282  fnmptd  15366  bj-charfun  15369  bj-charfundc  15370  bj-charfunr  15372  pw1nct  15563  nnsf  15565  nninfalllem1  15568  nninfall  15569  nninfself  15573  nninfsellemeq  15574  nninfsellemeqinf  15576  nninfsel  15577  isomninnlem  15590  trilpolemeq1  15600  trilpo  15603  apdiff  15608  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  redcwlpo  15615  redc0  15617  reap0  15618  dceqnconst  15620  dcapnconst  15621  nconstwlpolem  15625  nconstwlpo  15626  neapmkv  15628  ltlenmkv  15630