Theorem ralrimiva 2603

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralrimivvva  2613  rgen2  2616  rgen3  2617  nrexdv  2623  r19.29vva  2676  rabbidva  2787  ssrabdv  3303  ss2rabdv  3305  iuneq2dv  3986  iunssd  4011  disjeq2dv  4064  mpteq12dva  4165  triun  4195  issod  4410  frirrg  4441  frind  4443  peano2  4687  dmmptd  5454  fun11iun  5593  fniinfv  5692  eqfnfv  5732  eqfnfvd  5735  fnmptfvd  5739  dff3im  5780  dffo4  5783  fmptd  5789  ffnfv  5793  fmpt2d  5797  ffvresb  5798  funiun  5816  fconst2g  5854  fconstfvm  5857  resfunexg  5860  eufnfv  5870  foco2  5877  fniunfv  5886  fcofo  5908  fliftel  5917  fliftfun  5920  fliftfuns  5922  riota5f  5981  f1ocnvd  6208  suppssov1  6215  offval2  6234  ofrfval2  6235  offveqb  6238  offveq  6239  caofref  6243  caofinvl  6244  caofid0l  6245  caofid0r  6246  caofid1  6247  caofid2  6248  opabex3d  6266  uchoice  6283  oprssdmm  6317  f1od2  6381  disjxp1  6382  tfrlem1  6454  tfrlemisucaccv  6471  tfrlemiubacc  6476  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemubacc  6492  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemubacc  6505  tfrcllemaccex  6507  tfrcllemres  6508  tfrcl  6510  rdgon  6532  freccllem  6548  frecfcllem  6550  omcl  6607  oeicl  6608  qliftfuns  6766  ixpeq2dva  6860  xpf1o  7005  mapxpen  7009  isinfinf  7059  fimax2gtrilemstep  7062  undifdcss  7085  opabfi  7100  eqsuptid  7164  eqinftid  7188  difinfsnlem  7266  difinfsn  7267  ctmlemr  7275  ctm  7276  ctssdclemn0  7277  ctssdccl  7278  enumctlemm  7281  nninfninc  7290  nnnninf  7293  nnnninfeq  7295  enomnilem  7305  ismkvnex  7322  enmkvlem  7328  enwomnilem  7336  nninfwlporlemd  7339  nninfwlpoimlemg  7342  nninfwlpoimlemginf  7343  nninfwlpoim  7346  nninfinfwlpo  7347  finacn  7386  acfun  7389  exmidaclem  7390  exmidontriimlem4  7406  exmidontriim  7407  pw1on  7411  ccfunen  7450  cc2lem  7452  cc3  7454  acnccim  7458  genprndl  7708  genprndu  7709  nqprloc  7732  ltexprlemrnd  7792  ltexprlemdisj  7793  lteupri  7804  recexprlemrnd  7816  recexprlemdisj  7817  caucvgprlemlim  7868  caucvgprprlemlim  7898  suplocexprlemml  7903  suplocexprlemrl  7904  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  caucvgsrlembound  7981  caucvgsrlemgt1  7982  caucvgsrlemoffgt1  7986  caucvgsr  7989  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  elrealeu  8016  axcaucvglemcau  8085  axcaucvglemres  8086  axpre-suploclemres  8088  negeu  8337  eqord1  8630  eqord2  8631  creur  9106  creui  9107  suprzclex  9545  supinfneg  9790  infsupneg  9791  infregelbex  9793  indstr2  9804  iooidg  10105  iccsupr  10162  icoshftf1o  10187  fznlem  10237  exfzdc  10446  zsupcllemstep  10449  infssuzex  10453  suprzubdc  10456  zsupssdc  10458  exbtwnzlemstep  10467  exbtwnzlemex  10469  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgtcl  10634  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  frecuzrdgfunlem  10641  frecuzrdgsuctlem  10645  nninfinf  10665  iseqovex  10680  seq3val  10682  seqvalcd  10683  seq3-1  10684  seqf  10686  seq3p1  10687  seqovcd  10689  seqp1cd  10692  seq3clss  10693  seq3fveq2  10697  seqfveq2g  10699  seqfveqg  10700  seq3fveq  10701  seq3feq  10702  seq3shft2  10703  seqshft2g  10704  monoord  10707  monoord2  10708  ser3mono  10709  seq3split  10710  seqsplitg  10711  seq3caopr3  10713  seqcaopr3g  10714  seq3caopr2  10715  seqcaopr2g  10716  iseqf1olemqk  10729  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seq3f1oleml  10738  seq3f1o  10739  seqf1og  10743  seq3id3  10746  seq3id  10747  seq3id2  10748  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  ser3ge0  10758  nn0ltexp2  10931  bccl  10989  hashinfuni  10999  hashennnuni  11001  wrdexg  11082  ccatlen  11130  ccatvalfn  11136  ccatrn  11144  swrdlen  11184  swrdwrdsymbg  11196  swrdswrd  11237  wrdind  11254  reuccatpfxs1  11279  shftf  11341  seq3shft  11349  caucvgrelemcau  11491  cvg1nlemcau  11495  cvg1nlemres  11496  resqrexlemcvg  11530  resqrexlemglsq  11533  resqrexlemga  11534  maxabslemval  11719  negfi  11739  minmax  11741  xrmaxiflemval  11761  xrminmax  11776  climconst  11801  2clim  11812  climcn1  11819  climcn2  11820  reccn2ap  11824  cn1lem  11825  climsqz  11846  climsqz2  11847  climcau  11858  climrecvg1n  11859  serf0  11863  sumeq2dv  11879  sumrbdclem  11888  fsum3cvg  11889  summodclem3  11891  summodclem2a  11892  zsumdc  11895  isum  11896  fsumgcl  11897  fsum3  11898  fsumf1o  11901  isumss  11902  fisumss  11903  isumss2  11904  fsum3cvg2  11905  fsumsersdc  11906  fsum3ser  11908  fsumcl2lem  11909  fsumadd  11917  fsumsplit  11918  fsumm1  11927  fsum1p  11929  isumclim3  11934  isummulc2  11937  sumsplitdc  11943  fsum2dlemstep  11945  fisumcom2  11949  fsumshftm  11956  fsummulc2  11959  fsumge1  11972  fsum00  11973  fsumabs  11976  telfsumo  11977  telfsumo2  11978  fsumparts  11981  fsumrelem  11982  fsumiun  11988  hashiun  11989  hash2iun  11990  binomlem  11994  isumshft  12001  isum1p  12003  isumnn0nn  12004  isumrpcl  12005  isumlessdc  12007  divcnv  12008  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemseq  12037  cvgratnnlemabsle  12038  cvgratnnlemfm  12040  cvgratnnlemrate  12041  cvgratnn  12042  cvgratz  12043  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  clim2prod  12050  prodeq2dv  12077  prodrbdclem  12082  fproddccvg  12083  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  iprodap  12091  fprodseq  12094  fprodf1o  12099  prodssdc  12100  fprodssdc  12101  fprodmul  12102  fprodsplit  12108  fprodm1  12109  fprod1p  12110  fprodm1s  12112  fprodp1s  12113  fprodunsn  12115  fprodcl2lem  12116  fprodabs  12127  fprodeq0  12128  fprodap0  12132  fprod2dlemstep  12133  fprodcom2fi  12137  fprodrec  12140  fprodmodd  12152  efcvgfsum  12178  dvdsssfz1  12363  bitsfi  12468  bitsinv1  12473  dvdsbnd  12477  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemle  12529  bezoutlemsup  12530  dfgcd3  12531  dfgcd2  12535  nnwodc  12557  uzwodc  12558  nnwosdc  12560  nninfctlemfo  12561  coprmgcdb  12610  prmdc  12652  isprm5  12664  isprm6  12669  phivalfi  12734  phibndlem  12738  dfphi2  12742  hashdvds  12743  phiprmpw  12744  phimullem  12747  eulerthlemfi  12750  dvdsfi  12761  hashgcdeq  12762  phisum  12763  reumodprminv  12776  pclemdc  12811  pc2dvds  12853  pcz  12855  pcprmpw2  12856  pcmptdvds  12868  pcprod  12869  pcfac  12873  qexpz  12875  prmpwdvds  12878  pockthg  12880  infpnlem2  12883  1arithlem4  12889  1arith  12890  4sqlemafi  12918  4sqlemffi  12919  4sqleminfi  12920  ennnfonelemex  12985  ennnfonelemfun  12988  ennnfonelemf1  12989  ennnfonelemnn0  12993  ennnfonelemim  12995  exmidunben  12997  ctinfomlemom  12998  ctinfom  12999  ctinf  13001  ctiunctlemudc  13008  ctiunctlemf  13009  ctiunctlemfo  13010  omctfn  13014  ssnnctlemct  13017  nninfdclemcl  13019  nninfdclemp1  13021  pwsbas  13325  imasival  13339  ismgmid2  13413  mgmidsssn0  13417  grpinvalem  13418  grpinva  13419  gsumress  13428  issgrpd  13445  prdsplusgsgrpcl  13447  sgrpidmndm  13453  ismndd  13470  mndpfo  13471  prdsplusgcl  13479  prdsidlem  13480  mhmima  13524  mhmeql  13525  gsumvallem2  13526  isgrpd2e  13553  dfgrp2  13560  grpidd2  13574  isgrpinv  13587  grplrinv  13590  grpidinv  13592  dfgrp3me  13633  prdsinvlem  13641  mhmmnd  13653  ghmgrp  13655  mulgsubcl  13673  issubg2m  13726  issubgrpd2  13727  grpissubg  13731  subgintm  13735  nmzsubg  13747  ssnmz  13748  ghmrn  13794  ghmeql  13804  ghmf1  13810  conjnmz  13816  conjnmzb  13817  rinvmod  13846  srgrz  13947  srglz  13948  srgisid  13949  ringsrg  14010  rhmdvdsr  14139  rhmopp  14140  subrngintm  14176  subrg1  14195  subrgugrp  14204  subrgintm  14207  unitrrg  14231  aprap  14250  islmodd  14257  lssuni  14327  lsssubg  14341  lssintclm  14348  dflidl2rng  14445  lidlsubg  14450  cnsubglem  14543  gsumfzfsumlemm  14551  znf1o  14615  znidomb  14622  psrbagfi  14637  psr1clfi  14652  mplsubgfilemm  14662  mplsubgfilemcl  14663  mplsubgfi  14665  fiinbas  14723  tgclb  14739  restbasg  14842  iscnp4  14892  cnco  14895  cnptopco  14896  cnss1  14900  cnss2  14901  cncnpi  14902  cncnp  14904  cnconst2  14907  cnrest  14909  cnptopresti  14912  cnpdis  14916  lmtopcnp  14924  txbasval  14941  tx1cn  14943  tx2cn  14944  txcnp  14945  upxp  14946  txdis1cn  14952  cnmpt11  14957  psmet0  15001  psmettri2  15002  psmetxrge0  15006  psmetres2  15007  ismeti  15020  xmetpsmet  15043  blsscls2  15167  comet  15173  xmettx  15184  tgioo  15228  tgqioo  15229  fsumcncntop  15241  elcncf1di  15253  cdivcncfap  15278  mulcncflem  15281  mulcncf  15282  cnopnap  15285  divcncfap  15288  dedekindeulemuub  15291  dedekindeulemlu  15295  suplociccreex  15298  suplociccex  15299  dedekindicclemuub  15300  dedekindicclemlu  15304  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemdisj  15314  ivthinclemloc  15315  ivthinc  15317  ivthdec  15318  dich0  15326  ivthdich  15327  cnplimclemr  15343  limccnp2cntop  15351  limccoap  15352  dvcn  15374  dvfre  15384  dvrecap  15387  dvmptclx  15392  dvmptaddx  15393  dvmptmulx  15394  dveflem  15400  dvef  15401  ply1termlem  15416  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  plycj  15435  plyreres  15438  dvply1  15439  sin0pilem1  15455  sin0pilem2  15456  mpodvdsmulf1o  15664  mersenne  15671  perfectlem2  15674  lgsval2lem  15689  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem1f1o  15739  gausslemma2dlem2  15741  gausslemma2dlem3  15742  lgsquadlemofi  15755  lgsquadlem1  15756  lgsquadlem2  15757  2lgslem1a1  15765  2sqlem6  15799  2sqlem8  15802  2sqlem10  15804  usgruspgrben  15984  uspgredg2v  16019  usgredg2v  16022  wlk1walkdom  16070  fnmptd  16168  bj-charfun  16170  bj-charfundc  16171  bj-charfunr  16173  2omap  16359  pw1nct  16369  nnsf  16371  nninfalllem1  16374  nninfall  16375  nninfself  16379  nninfsellemeq  16380  nninfsellemeqinf  16382  nninfsel  16383  nnnninfex  16388  nninfnfiinf  16389  isomninnlem  16398  trilpolemeq1  16408  trilpo  16411  apdiff  16416  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420  redcwlpo  16423  redc0  16425  reap0  16426  dceqnconst  16428  dcapnconst  16429  nconstwlpolem  16433  nconstwlpo  16434  neapmkv  16436  ltlenmkv  16438