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  2788  ssrabdv  3304  ss2rabdv  3306  iuneq2dv  3989  iunssd  4014  disjeq2dv  4067  mpteq12dva  4168  triun  4198  issod  4414  frirrg  4445  frind  4447  peano2  4691  dmmptd  5460  fun11iun  5601  fniinfv  5700  eqfnfv  5740  eqfnfvd  5743  fnmptfvd  5747  dff3im  5788  dffo4  5791  fmptd  5797  ffnfv  5801  fmpt2d  5805  ffvresb  5806  funiun  5824  fconst2g  5864  fconstfvm  5867  resfunexg  5870  eufnfv  5880  foco2  5889  fniunfv  5898  fcofo  5920  fliftel  5929  fliftfun  5932  fliftfuns  5934  riota5f  5993  f1ocnvd  6220  suppssov1  6227  offval2  6246  ofrfval2  6247  offveqb  6250  offveq  6251  caofref  6255  caofinvl  6256  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  opabex3d  6278  uchoice  6295  oprssdmm  6329  f1od2  6395  disjxp1  6396  tfrlem1  6469  tfrlemisucaccv  6486  tfrlemiubacc  6491  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemubacc  6507  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemubacc  6520  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  rdgon  6547  freccllem  6563  frecfcllem  6565  omcl  6624  oeicl  6625  qliftfuns  6783  ixpeq2dva  6877  xpf1o  7025  mapxpen  7029  isinfinf  7079  fimax2gtrilemstep  7083  undifdcss  7108  opabfi  7123  eqsuptid  7187  eqinftid  7211  difinfsnlem  7289  difinfsn  7290  ctmlemr  7298  ctm  7299  ctssdclemn0  7300  ctssdccl  7301  enumctlemm  7304  nninfninc  7313  nnnninf  7316  nnnninfeq  7318  enomnilem  7328  ismkvnex  7345  enmkvlem  7351  enwomnilem  7359  nninfwlporlemd  7362  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  nninfwlpoim  7369  nninfinfwlpo  7370  finacn  7409  acfun  7412  exmidaclem  7413  exmidontriimlem4  7429  exmidontriim  7430  pw1on  7434  ccfunen  7473  cc2lem  7475  cc3  7477  acnccim  7481  genprndl  7731  genprndu  7732  nqprloc  7755  ltexprlemrnd  7815  ltexprlemdisj  7816  lteupri  7827  recexprlemrnd  7839  recexprlemdisj  7840  caucvgprlemlim  7891  caucvgprprlemlim  7921  suplocexprlemml  7926  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  caucvgsrlembound  8004  caucvgsrlemgt1  8005  caucvgsrlemoffgt1  8009  caucvgsr  8012  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  elrealeu  8039  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  negeu  8360  eqord1  8653  eqord2  8654  creur  9129  creui  9130  suprzclex  9568  supinfneg  9819  infsupneg  9820  infregelbex  9822  indstr2  9833  iooidg  10134  iccsupr  10191  icoshftf1o  10216  fznlem  10266  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  zsupssdc  10488  exbtwnzlemstep  10497  exbtwnzlemex  10499  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgtcl  10664  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  frecuzrdgfunlem  10671  frecuzrdgsuctlem  10675  nninfinf  10695  iseqovex  10710  seq3val  10712  seqvalcd  10713  seq3-1  10714  seqf  10716  seq3p1  10717  seqovcd  10719  seqp1cd  10722  seq3clss  10723  seq3fveq2  10727  seqfveq2g  10729  seqfveqg  10730  seq3fveq  10731  seq3feq  10732  seq3shft2  10733  seqshft2g  10734  monoord  10737  monoord2  10738  ser3mono  10739  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seq3caopr2  10745  seqcaopr2g  10746  iseqf1olemqk  10759  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1oleml  10768  seq3f1o  10769  seqf1og  10773  seq3id3  10776  seq3id  10777  seq3id2  10778  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  ser3ge0  10788  nn0ltexp2  10961  bccl  11019  hashinfuni  11029  hashennnuni  11031  wrdexg  11114  ccatlen  11162  ccatvalfn  11168  ccatrn  11176  swrdlen  11223  swrdwrdsymbg  11235  swrdswrd  11276  wrdind  11293  reuccatpfxs1  11318  shftf  11381  seq3shft  11389  caucvgrelemcau  11531  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemcvg  11570  resqrexlemglsq  11573  resqrexlemga  11574  maxabslemval  11759  negfi  11779  minmax  11781  xrmaxiflemval  11801  xrminmax  11816  climconst  11841  2clim  11852  climcn1  11859  climcn2  11860  reccn2ap  11864  cn1lem  11865  climsqz  11886  climsqz2  11887  climcau  11898  climrecvg1n  11899  serf0  11903  sumeq2dv  11919  sumrbdclem  11928  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  zsumdc  11935  isum  11936  fsumgcl  11937  fsum3  11938  fsumf1o  11941  isumss  11942  fisumss  11943  isumss2  11944  fsum3cvg2  11945  fsumsersdc  11946  fsum3ser  11948  fsumcl2lem  11949  fsumadd  11957  fsumsplit  11958  fsumm1  11967  fsum1p  11969  isumclim3  11974  isummulc2  11977  sumsplitdc  11983  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fsummulc2  11999  fsumge1  12012  fsum00  12013  fsumabs  12016  telfsumo  12017  telfsumo2  12018  fsumparts  12021  fsumrelem  12022  fsumiun  12028  hashiun  12029  hash2iun  12030  binomlem  12034  isumshft  12041  isum1p  12043  isumnn0nn  12044  isumrpcl  12045  isumlessdc  12047  divcnv  12048  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  clim2prod  12090  prodeq2dv  12117  prodrbdclem  12122  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  iprodap  12131  fprodseq  12134  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodmul  12142  fprodsplit  12148  fprodm1  12149  fprod1p  12150  fprodm1s  12152  fprodp1s  12153  fprodunsn  12155  fprodcl2lem  12156  fprodabs  12167  fprodeq0  12168  fprodap0  12172  fprod2dlemstep  12173  fprodcom2fi  12177  fprodrec  12180  fprodmodd  12192  efcvgfsum  12218  dvdsssfz1  12403  bitsfi  12508  bitsinv1  12513  dvdsbnd  12517  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemle  12569  bezoutlemsup  12570  dfgcd3  12571  dfgcd2  12575  nnwodc  12597  uzwodc  12598  nnwosdc  12600  nninfctlemfo  12601  coprmgcdb  12650  prmdc  12692  isprm5  12704  isprm6  12709  phivalfi  12774  phibndlem  12778  dfphi2  12782  hashdvds  12783  phiprmpw  12784  phimullem  12787  eulerthlemfi  12790  dvdsfi  12801  hashgcdeq  12802  phisum  12803  reumodprminv  12816  pclemdc  12851  pc2dvds  12893  pcz  12895  pcprmpw2  12896  pcmptdvds  12908  pcprod  12909  pcfac  12913  qexpz  12915  prmpwdvds  12918  pockthg  12920  infpnlem2  12923  1arithlem4  12929  1arith  12930  4sqlemafi  12958  4sqlemffi  12959  4sqleminfi  12960  ennnfonelemex  13025  ennnfonelemfun  13028  ennnfonelemf1  13029  ennnfonelemnn0  13033  ennnfonelemim  13035  exmidunben  13037  ctinfomlemom  13038  ctinfom  13039  ctinf  13041  ctiunctlemudc  13048  ctiunctlemf  13049  ctiunctlemfo  13050  omctfn  13054  ssnnctlemct  13057  nninfdclemcl  13059  nninfdclemp1  13061  pwsbas  13365  imasival  13379  ismgmid2  13453  mgmidsssn0  13457  grpinvalem  13458  grpinva  13459  gsumress  13468  issgrpd  13485  prdsplusgsgrpcl  13487  sgrpidmndm  13493  ismndd  13510  mndpfo  13511  prdsplusgcl  13519  prdsidlem  13520  mhmima  13564  mhmeql  13565  gsumvallem2  13566  isgrpd2e  13593  dfgrp2  13600  grpidd2  13614  isgrpinv  13627  grplrinv  13630  grpidinv  13632  dfgrp3me  13673  prdsinvlem  13681  mhmmnd  13693  ghmgrp  13695  mulgsubcl  13713  issubg2m  13766  issubgrpd2  13767  grpissubg  13771  subgintm  13775  nmzsubg  13787  ssnmz  13788  ghmrn  13834  ghmeql  13844  ghmf1  13850  conjnmz  13856  conjnmzb  13857  rinvmod  13886  srgrz  13987  srglz  13988  srgisid  13989  ringsrg  14050  rhmdvdsr  14179  rhmopp  14180  subrngintm  14216  subrg1  14235  subrgugrp  14244  subrgintm  14247  unitrrg  14271  aprap  14290  islmodd  14297  lssuni  14367  lsssubg  14381  lssintclm  14388  dflidl2rng  14485  lidlsubg  14490  cnsubglem  14583  gsumfzfsumlemm  14591  znf1o  14655  znidomb  14662  psrbagfi  14677  psr1clfi  14692  mplsubgfilemm  14702  mplsubgfilemcl  14703  mplsubgfi  14705  fiinbas  14763  tgclb  14779  restbasg  14882  iscnp4  14932  cnco  14935  cnptopco  14936  cnss1  14940  cnss2  14941  cncnpi  14942  cncnp  14944  cnconst2  14947  cnrest  14949  cnptopresti  14952  cnpdis  14956  lmtopcnp  14964  txbasval  14981  tx1cn  14983  tx2cn  14984  txcnp  14985  upxp  14986  txdis1cn  14992  cnmpt11  14997  psmet0  15041  psmettri2  15042  psmetxrge0  15046  psmetres2  15047  ismeti  15060  xmetpsmet  15083  blsscls2  15207  comet  15213  xmettx  15224  tgioo  15268  tgqioo  15269  fsumcncntop  15281  elcncf1di  15293  cdivcncfap  15318  mulcncflem  15321  mulcncf  15322  cnopnap  15325  divcncfap  15328  dedekindeulemuub  15331  dedekindeulemlu  15335  suplociccreex  15338  suplociccex  15339  dedekindicclemuub  15340  dedekindicclemlu  15344  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemdisj  15354  ivthinclemloc  15355  ivthinc  15357  ivthdec  15358  dich0  15366  ivthdich  15367  cnplimclemr  15383  limccnp2cntop  15391  limccoap  15392  dvcn  15414  dvfre  15424  dvrecap  15427  dvmptclx  15432  dvmptaddx  15433  dvmptmulx  15434  dveflem  15440  dvef  15441  ply1termlem  15456  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  plycj  15475  plyreres  15478  dvply1  15479  sin0pilem1  15495  sin0pilem2  15496  mpodvdsmulf1o  15704  mersenne  15711  perfectlem2  15714  lgsval2lem  15729  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1f1o  15779  gausslemma2dlem2  15781  gausslemma2dlem3  15782  lgsquadlemofi  15795  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1a1  15805  2sqlem6  15839  2sqlem8  15842  2sqlem10  15844  usgruspgrben  16025  uspgredg2v  16060  usgredg2v  16063  vtxedgfi  16095  vtxlpfi  16096  wlk1walkdom  16156  wlkres  16174  fnmptd  16336  bj-charfun  16338  bj-charfundc  16339  bj-charfunr  16341  2omap  16530  pw1nct  16540  nnsf  16543  nninfalllem1  16546  nninfall  16547  nninfself  16551  nninfsellemeq  16552  nninfsellemeqinf  16554  nninfsel  16555  nnnninfex  16560  nninfnfiinf  16561  isomninnlem  16570  trilpolemeq1  16580  trilpo  16583  apdiff  16588  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  redcwlpo  16595  redc0  16597  reap0  16598  dceqnconst  16600  dcapnconst  16601  nconstwlpolem  16605  nconstwlpo  16606  neapmkv  16608  ltlenmkv  16610