Theorem ralrimiva 2605

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∀wral 2510

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralrimivvva  2615  rgen2  2618  rgen3  2619  nrexdv  2625  r19.29vva  2678  rabbidva  2790  ssrabdv  3306  ss2rabdv  3308  iuneq2dv  3991  iunssd  4016  disjeq2dv  4069  mpteq12dva  4170  triun  4200  issod  4416  frirrg  4447  frind  4449  peano2  4693  dmmptd  5463  fun11iun  5604  fniinfv  5704  eqfnfv  5744  eqfnfvd  5747  fnmptfvd  5751  dff3im  5792  dffo4  5795  fmptd  5801  ffnfv  5805  fmpt2d  5809  ffvresb  5810  funiun  5829  fconst2g  5869  fconstfvm  5872  resfunexg  5875  eufnfv  5885  foco2  5894  fniunfv  5903  fcofo  5925  fliftel  5934  fliftfun  5937  fliftfuns  5939  riota5f  5998  f1ocnvd  6225  suppssov1  6232  offval2  6251  ofrfval2  6252  offveqb  6255  offveq  6256  caofref  6260  caofinvl  6261  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  opabex3d  6283  uchoice  6300  oprssdmm  6334  f1od2  6400  disjxp1  6401  tfrlem1  6474  tfrlemisucaccv  6491  tfrlemiubacc  6496  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  rdgon  6552  freccllem  6568  frecfcllem  6570  omcl  6629  oeicl  6630  qliftfuns  6788  ixpeq2dva  6882  xpf1o  7030  mapxpen  7034  isinfinf  7086  fimax2gtrilemstep  7090  undifdcss  7115  opabfi  7132  eqsuptid  7196  eqinftid  7220  difinfsnlem  7298  difinfsn  7299  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  enumctlemm  7313  nninfninc  7322  nnnninf  7325  nnnninfeq  7327  enomnilem  7337  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  nninfwlporlemd  7371  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  finacn  7419  acfun  7422  exmidaclem  7423  exmidontriimlem4  7439  exmidontriim  7440  pw1on  7444  ccfunen  7483  cc2lem  7485  cc3  7487  acnccim  7491  genprndl  7741  genprndu  7742  nqprloc  7765  ltexprlemrnd  7825  ltexprlemdisj  7826  lteupri  7837  recexprlemrnd  7849  recexprlemdisj  7850  caucvgprlemlim  7901  caucvgprprlemlim  7931  suplocexprlemml  7936  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  caucvgsrlembound  8014  caucvgsrlemgt1  8015  caucvgsrlemoffgt1  8019  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  elrealeu  8049  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  negeu  8370  eqord1  8663  eqord2  8664  creur  9139  creui  9140  suprzclex  9578  supinfneg  9829  infsupneg  9830  infregelbex  9832  indstr2  9843  iooidg  10144  iccsupr  10201  icoshftf1o  10226  fznlem  10276  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  zsupssdc  10499  exbtwnzlemstep  10508  exbtwnzlemex  10510  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  nninfinf  10706  iseqovex  10721  seq3val  10723  seqvalcd  10724  seq3-1  10725  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seqfveqg  10741  seq3fveq  10742  seq3feq  10743  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1og  10784  seq3id3  10787  seq3id  10788  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  nn0ltexp2  10972  bccl  11030  hashinfuni  11040  hashennnuni  11042  wrdexg  11128  ccatlen  11176  ccatvalfn  11182  ccatrn  11190  swrdlen  11237  swrdwrdsymbg  11249  swrdswrd  11290  wrdind  11307  reuccatpfxs1  11332  shftf  11408  seq3shft  11416  caucvgrelemcau  11558  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemcvg  11597  resqrexlemglsq  11600  resqrexlemga  11601  maxabslemval  11786  negfi  11806  minmax  11808  xrmaxiflemval  11828  xrminmax  11843  climconst  11868  2clim  11879  climcn1  11886  climcn2  11887  reccn2ap  11891  cn1lem  11892  climsqz  11913  climsqz2  11914  climcau  11925  climrecvg1n  11926  serf0  11930  sumeq2dv  11946  sumrbdclem  11956  fsum3cvg  11957  summodclem3  11959  summodclem2a  11960  zsumdc  11963  isum  11964  fsumgcl  11965  fsum3  11966  fsumf1o  11969  isumss  11970  fisumss  11971  isumss2  11972  fsum3cvg2  11973  fsumsersdc  11974  fsum3ser  11976  fsumcl2lem  11977  fsumadd  11985  fsumsplit  11986  fsumm1  11995  fsum1p  11997  isumclim3  12002  isummulc2  12005  sumsplitdc  12011  fsum2dlemstep  12013  fisumcom2  12017  fsumshftm  12024  fsummulc2  12027  fsumge1  12040  fsum00  12041  fsumabs  12044  telfsumo  12045  telfsumo2  12046  fsumparts  12049  fsumrelem  12050  fsumiun  12056  hashiun  12057  hash2iun  12058  binomlem  12062  isumshft  12069  isum1p  12071  isumnn0nn  12072  isumrpcl  12073  isumlessdc  12075  divcnv  12076  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemseq  12105  cvgratnnlemabsle  12106  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratnn  12110  cvgratz  12111  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  clim2prod  12118  prodeq2dv  12145  prodrbdclem  12150  fproddccvg  12151  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  iprodap  12159  fprodseq  12162  fprodf1o  12167  prodssdc  12168  fprodssdc  12169  fprodmul  12170  fprodsplit  12176  fprodm1  12177  fprod1p  12178  fprodm1s  12180  fprodp1s  12181  fprodunsn  12183  fprodcl2lem  12184  fprodabs  12195  fprodeq0  12196  fprodap0  12200  fprod2dlemstep  12201  fprodcom2fi  12205  fprodrec  12208  fprodmodd  12220  efcvgfsum  12246  dvdsssfz1  12431  bitsfi  12536  bitsinv1  12541  dvdsbnd  12545  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemle  12597  bezoutlemsup  12598  dfgcd3  12599  dfgcd2  12603  nnwodc  12625  uzwodc  12626  nnwosdc  12628  nninfctlemfo  12629  coprmgcdb  12678  prmdc  12720  isprm5  12732  isprm6  12737  phivalfi  12802  phibndlem  12806  dfphi2  12810  hashdvds  12811  phiprmpw  12812  phimullem  12815  eulerthlemfi  12818  dvdsfi  12829  hashgcdeq  12830  phisum  12831  reumodprminv  12844  pclemdc  12879  pc2dvds  12921  pcz  12923  pcprmpw2  12924  pcmptdvds  12936  pcprod  12937  pcfac  12941  qexpz  12943  prmpwdvds  12946  pockthg  12948  infpnlem2  12951  1arithlem4  12957  1arith  12958  4sqlemafi  12986  4sqlemffi  12987  4sqleminfi  12988  ennnfonelemex  13053  ennnfonelemfun  13056  ennnfonelemf1  13057  ennnfonelemnn0  13061  ennnfonelemim  13063  exmidunben  13065  ctinfomlemom  13066  ctinfom  13067  ctinf  13069  ctiunctlemudc  13076  ctiunctlemf  13077  ctiunctlemfo  13078  omctfn  13082  ssnnctlemct  13085  nninfdclemcl  13087  nninfdclemp1  13089  pwsbas  13393  imasival  13407  ismgmid2  13481  mgmidsssn0  13485  grpinvalem  13486  grpinva  13487  gsumress  13496  issgrpd  13513  prdsplusgsgrpcl  13515  sgrpidmndm  13521  ismndd  13538  mndpfo  13539  prdsplusgcl  13547  prdsidlem  13548  mhmima  13592  mhmeql  13593  gsumvallem2  13594  isgrpd2e  13621  dfgrp2  13628  grpidd2  13642  isgrpinv  13655  grplrinv  13658  grpidinv  13660  dfgrp3me  13701  prdsinvlem  13709  mhmmnd  13721  ghmgrp  13723  mulgsubcl  13741  issubg2m  13794  issubgrpd2  13795  grpissubg  13799  subgintm  13803  nmzsubg  13815  ssnmz  13816  ghmrn  13862  ghmeql  13872  ghmf1  13878  conjnmz  13884  conjnmzb  13885  rinvmod  13914  srgrz  14016  srglz  14017  srgisid  14018  ringsrg  14079  rhmdvdsr  14208  rhmopp  14209  subrngintm  14245  subrg1  14264  subrgugrp  14273  subrgintm  14276  unitrrg  14300  aprap  14319  islmodd  14326  lssuni  14396  lsssubg  14410  lssintclm  14417  dflidl2rng  14514  lidlsubg  14519  cnsubglem  14612  gsumfzfsumlemm  14620  znf1o  14684  znidomb  14691  psrbagfi  14706  psr1clfi  14721  mplsubgfilemm  14731  mplsubgfilemcl  14732  mplsubgfi  14734  fiinbas  14792  tgclb  14808  restbasg  14911  iscnp4  14961  cnco  14964  cnptopco  14965  cnss1  14969  cnss2  14970  cncnpi  14971  cncnp  14973  cnconst2  14976  cnrest  14978  cnptopresti  14981  cnpdis  14985  lmtopcnp  14993  txbasval  15010  tx1cn  15012  tx2cn  15013  txcnp  15014  upxp  15015  txdis1cn  15021  cnmpt11  15026  psmet0  15070  psmettri2  15071  psmetxrge0  15075  psmetres2  15076  ismeti  15089  xmetpsmet  15112  blsscls2  15236  comet  15242  xmettx  15253  tgioo  15297  tgqioo  15298  fsumcncntop  15310  elcncf1di  15322  cdivcncfap  15347  mulcncflem  15350  mulcncf  15351  cnopnap  15354  divcncfap  15357  dedekindeulemuub  15360  dedekindeulemlu  15364  suplociccreex  15367  suplociccex  15368  dedekindicclemuub  15369  dedekindicclemlu  15373  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemdisj  15383  ivthinclemloc  15384  ivthinc  15386  ivthdec  15387  dich0  15395  ivthdich  15396  cnplimclemr  15412  limccnp2cntop  15420  limccoap  15421  dvcn  15443  dvfre  15453  dvrecap  15456  dvmptclx  15461  dvmptaddx  15462  dvmptmulx  15463  dveflem  15469  dvef  15470  ply1termlem  15485  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  plycj  15504  plyreres  15507  dvply1  15508  sin0pilem1  15524  sin0pilem2  15525  mpodvdsmulf1o  15733  mersenne  15740  perfectlem2  15743  lgsval2lem  15758  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1f1o  15808  gausslemma2dlem2  15810  gausslemma2dlem3  15811  lgsquadlemofi  15824  lgsquadlem1  15825  lgsquadlem2  15826  2lgslem1a1  15834  2sqlem6  15868  2sqlem8  15871  2sqlem10  15873  usgruspgrben  16056  uspgredg2v  16091  usgredg2v  16094  subuhgr  16142  subupgr  16143  subumgr  16144  subusgr  16145  vtxedgfi  16159  vtxlpfi  16160  wlk1walkdom  16229  wlkres  16249  eupth2lembfi  16347  depindlem1  16376  depindlem2  16377  depindlem3  16378  fnmptd  16451  bj-charfun  16453  bj-charfundc  16454  bj-charfunr  16456  2omap  16645  pw1nct  16655  nnsf  16658  nninfalllem1  16661  nninfall  16662  nninfself  16666  nninfsellemeq  16667  nninfsellemeqinf  16669  nninfsel  16670  nnnninfex  16675  nninfnfiinf  16676  isomninnlem  16685  trilpolemeq1  16695  trilpo  16698  apdiff  16703  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  redcwlpo  16711  redc0  16713  reap0  16714  dceqnconst  16716  dcapnconst  16717  nconstwlpolem  16721  nconstwlpo  16722  neapmkv  16724  ltlenmkv  16726