Theorem ralrimiva 2548

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2146  ∀wral 2453

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458

This theorem is referenced by:  ralrimivvva  2558  rgen2  2561  rgen3  2562  nrexdv  2568  r19.29vva  2620  rabbidva  2723  ssrabdv  3232  ss2rabdv  3234  iuneq2dv  3903  disjeq2dv  3980  mpteq12dva  4079  triun  4109  issod  4313  frirrg  4344  frind  4346  peano2  4588  dmmptd  5338  fun11iun  5474  fniinfv  5566  eqfnfv  5605  eqfnfvd  5608  fnmptfvd  5612  dff3im  5653  dffo4  5656  fmptd  5662  ffnfv  5666  fmpt2d  5670  ffvresb  5671  fconst2g  5723  fconstfvm  5726  resfunexg  5729  eufnfv  5738  foco2  5745  fniunfv  5753  fcofo  5775  fliftel  5784  fliftfun  5787  fliftfuns  5789  riota5f  5845  f1ocnvd  6063  suppssov1  6070  offval2  6088  ofrfval2  6089  offveqb  6092  caofref  6094  caofinvl  6095  opabex3d  6112  oprssdmm  6162  f1od2  6226  disjxp1  6227  tfrlem1  6299  tfrlemisucaccv  6316  tfrlemiubacc  6321  tfr1onlemsucfn  6331  tfr1onlemsucaccv  6332  tfr1onlembxssdm  6334  tfr1onlembfn  6335  tfr1onlemubacc  6337  tfr1onlemaccex  6339  tfr1onlemres  6340  tfrcllemsucfn  6344  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllembfn  6348  tfrcllemubacc  6350  tfrcllemaccex  6352  tfrcllemres  6353  tfrcl  6355  rdgon  6377  freccllem  6393  frecfcllem  6395  omcl  6452  oeicl  6453  qliftfuns  6609  ixpeq2dva  6703  xpf1o  6834  mapxpen  6838  isinfinf  6887  fimax2gtrilemstep  6890  undifdcss  6912  eqsuptid  6986  eqinftid  7010  difinfsnlem  7088  difinfsn  7089  ctmlemr  7097  ctm  7098  ctssdclemn0  7099  ctssdccl  7100  enumctlemm  7103  nnnninf  7114  nnnninfeq  7116  enomnilem  7126  ismkvnex  7143  enmkvlem  7149  enwomnilem  7157  nninfwlporlemd  7160  nninfwlpoimlemg  7163  nninfwlpoimlemginf  7164  nninfwlpoim  7166  acfun  7196  exmidaclem  7197  exmidontriimlem4  7213  exmidontriim  7214  pw1on  7215  ccfunen  7238  cc2lem  7240  cc3  7242  genprndl  7495  genprndu  7496  nqprloc  7519  ltexprlemrnd  7579  ltexprlemdisj  7580  lteupri  7591  recexprlemrnd  7603  recexprlemdisj  7604  caucvgprlemlim  7655  caucvgprprlemlim  7685  suplocexprlemml  7690  suplocexprlemrl  7691  suplocexprlemmu  7692  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemub  7697  caucvgsrlembound  7768  caucvgsrlemgt1  7769  caucvgsrlemoffgt1  7773  caucvgsr  7776  suplocsrlemb  7780  suplocsrlempr  7781  suplocsrlem  7782  elrealeu  7803  axcaucvglemcau  7872  axcaucvglemres  7873  axpre-suploclemres  7875  negeu  8122  eqord1  8414  eqord2  8415  creur  8889  creui  8890  suprzclex  9324  supinfneg  9568  infsupneg  9569  infregelbex  9571  indstr2  9582  iooidg  9880  iccsupr  9937  icoshftf1o  9962  fznlem  10011  exfzdc  10210  exbtwnzlemstep  10218  exbtwnzlemex  10220  frec2uzrdg  10379  frecuzrdgrcl  10380  frecuzrdgtcl  10382  frecuzrdgsuc  10384  frecuzrdgrclt  10385  frecuzrdgg  10386  frecuzrdgfunlem  10389  frecuzrdgsuctlem  10393  iseqovex  10426  seq3val  10428  seqvalcd  10429  seq3-1  10430  seqf  10431  seq3p1  10432  seqovcd  10433  seqp1cd  10436  seq3clss  10437  seq3fveq2  10439  seq3fveq  10441  seq3feq  10442  seq3shft2  10443  monoord  10446  monoord2  10447  ser3mono  10448  seq3split  10449  seq3caopr3  10451  seq3caopr2  10452  iseqf1olemqk  10464  iseqf1olemjpcl  10465  iseqf1olemqpcl  10466  iseqf1olemfvp  10467  seq3f1olemqsumkj  10468  seq3f1olemqsumk  10469  seq3f1olemqsum  10470  seq3f1oleml  10473  seq3f1o  10474  seq3id3  10477  seq3id  10478  seq3id2  10479  seq3homo  10480  seq3z  10481  ser3ge0  10487  nn0ltexp2  10658  bccl  10715  hashinfuni  10725  hashennnuni  10727  shftf  10807  seq3shft  10815  caucvgrelemcau  10957  cvg1nlemcau  10961  cvg1nlemres  10962  resqrexlemcvg  10996  resqrexlemglsq  10999  resqrexlemga  11000  maxabslemval  11185  negfi  11204  minmax  11206  xrmaxiflemval  11226  xrminmax  11241  climconst  11266  2clim  11277  climcn1  11284  climcn2  11285  reccn2ap  11289  cn1lem  11290  climsqz  11311  climsqz2  11312  climcau  11323  climrecvg1n  11324  serf0  11328  sumeq2dv  11344  sumrbdclem  11353  fsum3cvg  11354  summodclem3  11356  summodclem2a  11357  zsumdc  11360  isum  11361  fsumgcl  11362  fsum3  11363  fsumf1o  11366  isumss  11367  fisumss  11368  isumss2  11369  fsum3cvg2  11370  fsumsersdc  11371  fsum3ser  11373  fsumcl2lem  11374  fsumadd  11382  fsumsplit  11383  fsumm1  11392  fsum1p  11394  isumclim3  11399  isummulc2  11402  sumsplitdc  11408  fsum2dlemstep  11410  fisumcom2  11414  fsumshftm  11421  fsummulc2  11424  fsumge1  11437  fsum00  11438  fsumabs  11441  telfsumo  11442  telfsumo2  11443  fsumparts  11446  fsumrelem  11447  fsumiun  11453  hashiun  11454  hash2iun  11455  binomlem  11459  isumshft  11466  isum1p  11468  isumnn0nn  11469  isumrpcl  11470  isumlessdc  11472  divcnv  11473  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  cvgratnnlemseq  11502  cvgratnnlemabsle  11503  cvgratnnlemfm  11505  cvgratnnlemrate  11506  cvgratnn  11507  cvgratz  11508  mertenslemi1  11511  mertenslem2  11512  mertensabs  11513  clim2prod  11515  prodeq2dv  11542  prodrbdclem  11547  fproddccvg  11548  prodmodclem3  11551  prodmodclem2a  11552  zproddc  11555  iprodap  11556  fprodseq  11559  fprodf1o  11564  prodssdc  11565  fprodssdc  11566  fprodmul  11567  fprodsplit  11573  fprodm1  11574  fprod1p  11575  fprodm1s  11577  fprodp1s  11578  fprodunsn  11580  fprodcl2lem  11581  fprodabs  11592  fprodeq0  11593  fprodap0  11597  fprod2dlemstep  11598  fprodcom2fi  11602  fprodrec  11605  fprodmodd  11617  efcvgfsum  11643  dvdsssfz1  11825  zsupcllemstep  11913  infssuzex  11917  suprzubdc  11920  zsupssdc  11922  dvdsbnd  11924  bezoutlemstep  11965  bezoutlemmain  11966  bezoutlemle  11976  bezoutlemsup  11977  dfgcd3  11978  dfgcd2  11982  nnwodc  12004  uzwodc  12005  nnwosdc  12007  coprmgcdb  12055  prmdc  12097  isprm5  12109  isprm6  12114  phivalfi  12179  phibndlem  12183  dfphi2  12187  hashdvds  12188  phiprmpw  12189  phimullem  12192  eulerthlemfi  12195  hashgcdeq  12206  phisum  12207  reumodprminv  12220  pclemdc  12255  pc2dvds  12296  pcz  12298  pcprmpw2  12299  pcmptdvds  12310  pcprod  12311  pcfac  12315  qexpz  12317  prmpwdvds  12320  pockthg  12322  infpnlem2  12325  1arithlem4  12331  1arith  12332  ennnfonelemex  12382  ennnfonelemfun  12385  ennnfonelemf1  12386  ennnfonelemnn0  12390  ennnfonelemim  12392  exmidunben  12394  ctinfomlemom  12395  ctinfom  12396  ctinf  12398  ctiunctlemudc  12405  ctiunctlemf  12406  ctiunctlemfo  12407  omctfn  12411  ssnnctlemct  12414  nninfdclemcl  12416  nninfdclemp1  12418  ismgmid2  12665  mgmidsssn0  12669  grprinvlem  12670  grprinvd  12671  sgrpidmndm  12687  ismndd  12704  mndpfo  12705  mhmima  12737  mhmeql  12738  isgrpd2e  12758  dfgrp2  12764  grpidd2  12776  isgrpinv  12788  grplrinv  12789  grpidinv  12791  dfgrp3me  12831  mhmmnd  12841  ghmgrp  12843  mulgsubcl  12858  rinvmod  12911  srgrz  12964  srglz  12965  srgisid  12966  ringsrg  13020  fiinbas  13118  tgclb  13136  restbasg  13239  iscnp4  13289  cnco  13292  cnptopco  13293  cnss1  13297  cnss2  13298  cncnpi  13299  cncnp  13301  cnconst2  13304  cnrest  13306  cnptopresti  13309  cnpdis  13313  lmtopcnp  13321  txbasval  13338  tx1cn  13340  tx2cn  13341  txcnp  13342  upxp  13343  txdis1cn  13349  cnmpt11  13354  psmet0  13398  psmettri2  13399  psmetxrge0  13403  psmetres2  13404  ismeti  13417  xmetpsmet  13440  blsscls2  13564  comet  13570  xmettx  13581  tgioo  13617  tgqioo  13618  fsumcncntop  13627  elcncf1di  13637  cdivcncfap  13658  mulcncflem  13661  mulcncf  13662  cnopnap  13665  dedekindeulemuub  13666  dedekindeulemlu  13670  suplociccreex  13673  suplociccex  13674  dedekindicclemuub  13675  dedekindicclemlu  13679  ivthinclemlopn  13685  ivthinclemlr  13686  ivthinclemuopn  13687  ivthinclemur  13688  ivthinclemdisj  13689  ivthinclemloc  13690  ivthinc  13692  ivthdec  13693  cnplimclemr  13709  limccnp2cntop  13717  limccoap  13718  dvcn  13735  dvfre  13745  dvrecap  13748  dvmptclx  13751  dvmptaddx  13752  dvmptmulx  13753  dveflem  13758  dvef  13759  sin0pilem1  13773  sin0pilem2  13774  lgsval2lem  13982  lgsdirnn0  14019  lgsdinn0  14020  2sqlem6  14027  2sqlem8  14030  2sqlem10  14032  fnmptd  14116  bj-charfun  14119  bj-charfundc  14120  bj-charfunr  14122  pw1nct  14313  nnsf  14315  nninfalllem1  14318  nninfall  14319  nninfself  14323  nninfsellemeq  14324  nninfsellemeqinf  14326  nninfsel  14327  isomninnlem  14339  trilpolemeq1  14349  trilpo  14352  apdiff  14357  iswomninnlem  14358  iswomni0  14360  ismkvnnlem  14361  redcwlpo  14364  redc0  14366  reap0  14367  dceqnconst  14368  dcapnconst  14369  nconstwlpolem  14373  nconstwlpo  14374  neapmkv  14376