Theorem ralrimiva 2623

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralrimivvva  2633  rgen2  2636  rgen3  2637  nrexdv  2643  r19.29vva  2696  rabbidva  2809  ssrabdv  3327  ss2rabdv  3329  iuneq2dv  4033  iunssd  4058  disjeq2dv  4111  mpteq12dva  4212  triun  4242  issod  4464  frirrg  4495  frind  4497  peano2  4742  dmmptd  5514  fun11iun  5660  fniinfv  5761  eqfnfv  5806  eqfnfvd  5809  fnmptfvd  5813  dff3im  5853  dffo4  5856  fmptd  5862  ffnfv  5866  fmpt2d  5870  ffvresb  5871  funiun  5890  fconst2g  5930  fconstfvm  5933  resfunexg  5936  eufnfv  5949  foco2  5959  fniunfv  5968  fcofo  5990  fliftel  5999  fliftfun  6002  fliftfuns  6004  riota5f  6065  f1ocnvd  6292  f1o3d  6298  suppssov1  6299  offval2  6318  ofrfval2  6319  offveqb  6322  offveq  6323  caofref  6327  caofinvl  6328  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  opabex3d  6350  uchoice  6371  oprssdmm  6405  f1od2  6471  disjxp1  6472  funsssuppss  6498  suppofss1dcl  6504  suppofss2dcl  6505  tfrlem1  6579  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  rdgon  6657  freccllem  6673  frecfcllem  6675  omcl  6734  oeicl  6735  qliftfuns  6893  ixpeq2dva  6995  xpf1o  7144  mapxpen  7148  isinfinf  7201  fimax2gtrilemstep  7205  undifdcss  7230  opabfi  7247  fissfi  7263  fdcf1  7316  f1setfi  7317  2omap  7318  eqsuptid  7337  eqinftid  7361  difinfsnlem  7439  difinfsn  7440  ctmlemr  7448  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  enumctlemm  7454  nninfninc  7463  nnnninf  7466  nnnninfeq  7468  enomnilem  7478  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  nninfwlporlemd  7512  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  nninfwlpoim  7519  nninfinfwlpo  7520  finacn  7560  acfun  7563  exmidaclem  7564  exmidontriimlem4  7580  exmidontriim  7581  pw1on  7585  ccfunen  7630  cc2lem  7632  cc3  7634  acnccim  7638  genprndl  7888  genprndu  7889  nqprloc  7912  ltexprlemrnd  7972  ltexprlemdisj  7973  lteupri  7984  recexprlemrnd  7996  recexprlemdisj  7997  caucvgprlemlim  8048  caucvgprprlemlim  8078  suplocexprlemml  8083  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  caucvgsrlembound  8161  caucvgsrlemgt1  8162  caucvgsrlemoffgt1  8166  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  elrealeu  8196  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  negeu  8517  eqord1  8811  eqord2  8812  creur  9289  creui  9290  suprzclex  9744  supinfneg  9995  infsupneg  9996  infregelbex  9998  indstr2  10009  iooidg  10311  iccsupr  10368  icoshftf1o  10393  fznlem  10445  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  suprzubdc  10671  zsupssdc  10673  exbtwnzlemstep  10682  exbtwnzlemex  10684  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgtcl  10849  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgfunlem  10856  frecuzrdgsuctlem  10860  nninfinf  10880  iseqovex  10895  seq3val  10897  seqvalcd  10898  seq3-1  10899  seqf  10901  seq3p1  10902  seqovcd  10904  seqp1cd  10907  seq3clss  10908  seq3fveq2  10912  seqfveq2g  10914  seqfveqg  10915  seq3fveq  10916  seq3feq  10917  seq3shft2  10918  seqshft2g  10919  monoord  10922  monoord2  10923  ser3mono  10924  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seq3caopr2  10930  seqcaopr2g  10931  iseqf1olemqk  10944  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seq3f1oleml  10953  seq3f1o  10954  seqf1og  10958  seq3id3  10961  seq3id  10962  seq3id2  10963  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  ser3ge0  10973  nn0ltexp2  11147  bccl  11205  hashinfuni  11216  hashennnuni  11218  sshashneg  11281  hashfibclem  11282  hashf1lem1  11285  wrdexg  11315  ccatlen  11363  ccatvalfn  11369  ccatrn  11377  swrdlen  11424  swrdwrdsymbg  11436  swrdswrd  11477  wrdind  11494  reuccatpfxs1  11519  shftf  11595  seq3shft  11603  caucvgrelemcau  11746  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemcvg  11785  resqrexlemglsq  11788  resqrexlemga  11789  maxabslemval  11974  negfi  11994  minmax  11996  xrmaxiflemval  12016  xrminmax  12031  climconst  12056  2clim  12067  climcn1  12074  climcn2  12075  reccn2ap  12079  cn1lem  12080  climsqz  12101  climsqz2  12102  climcau  12113  climrecvg1n  12114  serf0  12118  sumeq2dv  12134  sumrbdclem  12144  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  zsumdc  12151  isum  12152  fsumgcl  12153  fsum3  12154  fsumf1o  12157  isumss  12158  fisumss  12159  isumss2  12160  fsum3cvg2  12161  fsumsersdc  12162  fsum3ser  12164  fsumcl2lem  12165  fsumadd  12173  fsumsplit  12174  fsumm1  12183  fsum1p  12185  isumclim3  12190  isummulc2  12193  sumsplitdc  12199  fsum2dlemstep  12201  fisumcom2  12205  fsumshftm  12212  fsummulc2  12215  fsumge1  12228  fsum00  12229  fsumabs  12232  telfsumo  12233  telfsumo2  12234  fsumparts  12237  fsumrelem  12238  fsumiun  12244  hashiun  12245  hash2iun  12246  binomlem  12250  isumshft  12257  isum1p  12259  isumnn0nn  12260  isumrpcl  12261  isumlessdc  12263  divcnv  12264  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemseq  12293  cvgratnnlemabsle  12294  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratnn  12298  cvgratz  12299  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  clim2prod  12306  prodeq2dv  12333  prodrbdclem  12338  fproddccvg  12339  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  iprodap  12347  fprodseq  12350  fprodf1o  12355  prodssdc  12356  fprodssdc  12357  fprodmul  12358  fprodsplit  12364  fprodm1  12365  fprod1p  12366  fprodm1s  12368  fprodp1s  12369  fprodunsn  12371  fprodcl2lem  12372  fprodabs  12383  fprodeq0  12384  fprodap0  12388  fprod2dlemstep  12389  fprodcom2fi  12393  fprodrec  12396  fprodmodd  12408  efcvgfsum  12434  dvdsssfz1  12619  bitsfi  12724  bitsinv1  12729  dvdsbnd  12733  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemle  12785  bezoutlemsup  12786  dfgcd3  12787  dfgcd2  12791  nnwodc  12813  uzwodc  12814  nnwosdc  12816  nninfctlemfo  12817  coprmgcdb  12866  prmdc  12908  isprm5  12920  isprm6  12925  phivalfi  12990  phibndlem  12994  dfphi2  12998  hashdvds  12999  phiprmpw  13000  phimullem  13003  eulerthlemfi  13006  dvdsfi  13017  hashgcdeq  13018  phisum  13019  reumodprminv  13032  pclemdc  13067  pc2dvds  13109  pcz  13111  pcprmpw2  13112  pcmptdvds  13124  pcprod  13125  pcfac  13129  qexpz  13131  prmpwdvds  13134  pockthg  13136  infpnlem2  13139  1arithlem4  13145  1arith  13146  4sqlemafi  13174  4sqlemffi  13175  4sqleminfi  13176  ballotfilemcinfi  13224  ballotfilemdifcfi  13225  ballotfilemcinfz  13226  ballotfilemdifcfz  13227  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemefi  13237  ballotfilemodife  13240  ballotfilemiex  13244  ennnfonelemex  13305  ennnfonelemfun  13308  ennnfonelemf1  13309  ennnfonelemnn0  13313  ennnfonelemim  13315  exmidunben  13317  ctinfomlemom  13318  ctinfom  13319  ctinf  13321  ctiunctlemudc  13328  ctiunctlemf  13329  ctiunctlemfo  13330  omctfn  13334  ssnnctlemct  13337  nninfdclemcl  13339  nninfdclemp1  13341  imasival  13627  ismgmid2  13700  mgmidsssn0  13704  grpinvalem  13705  grpinva  13706  gzsumress  13712  issgrpd  13727  sgrpidmndm  13733  ismndd  13750  mndpfo  13751  mhmima  13798  mhmeql  13799  gsumvallem2  13800  isgrpd2e  13825  dfgrp2  13832  grpidd2  13846  isgrpinv  13859  grplrinv  13862  grpidinv  13864  dfgrp3me  13905  mhmmnd  13919  ghmgrp  13921  mulgsubcl  13939  issubg2m  13992  issubgrpd2  13993  grpissubg  13997  subgintm  14001  nmzsubg  14013  ssnmz  14014  ghmrn  14060  ghmeql  14070  ghmf1  14076  conjnmz  14082  conjnmzb  14083  rinvmod  14113  gsummptfidmadd  14161  prdsplusgsgrpcl  14190  prdsplusgcl  14192  prdsidlem  14193  prdsinvlem  14196  pwsbas  14205  srgrz  14288  srglz  14289  srgisid  14290  ringsrg  14352  rhmdvdsr  14482  rhmopp  14483  subrngintm  14520  subrg1  14539  subrgugrp  14548  subrgintm  14551  rrgsupp  14574  unitrrg  14576  aprap  14598  islmodd  14629  lssuni  14700  lsssubg  14714  lssintclm  14721  dflidl2rng  14818  lidlsubg  14823  cnsubglem  14916  gsumfsum  14923  znf1o  14986  znidomb  14993  asclfnd  15023  psrbagfi  15059  psrbaglecl  15060  psrbagcon  15062  psr1clfi  15079  mplsubgfilemm  15089  mplsubgfilemcl  15090  mplsubgfi  15092  fiinbas  15150  tgclb  15166  restbasg  15269  iscnp4  15319  cnco  15322  cnptopco  15323  cnss1  15327  cnss2  15328  cncnpi  15329  cncnp  15331  cnconst2  15334  cnrest  15336  cnptopresti  15339  cnpdis  15343  lmtopcnp  15351  txbasval  15368  tx1cn  15370  tx2cn  15371  txcnp  15372  upxp  15373  txdis1cn  15379  cnmpt11  15384  psmet0  15428  psmettri2  15429  psmetxrge0  15433  psmetres2  15434  ismeti  15447  xmetpsmet  15470  blsscls2  15594  comet  15600  xmettx  15611  tgioo  15655  tgqioo  15656  fsumcncntop  15668  elcncf1di  15680  cdivcncfap  15705  mulcncflem  15708  mulcncf  15709  cnopnap  15712  divcncfap  15715  dedekindeulemuub  15718  dedekindeulemlu  15722  suplociccreex  15725  suplociccex  15726  dedekindicclemuub  15727  dedekindicclemlu  15731  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemdisj  15741  ivthinclemloc  15742  ivthinc  15744  ivthdec  15745  dich0  15753  ivthdich  15754  cnplimclemr  15770  limccnp2cntop  15778  limccoap  15779  dvcn  15801  dvfre  15811  dvrecap  15814  dvmptclx  15819  dvmptaddx  15820  dvmptmulx  15821  dveflem  15827  dvef  15828  ply1termlem  15843  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  plycj  15862  plyreres  15865  dvply1  15866  sin0pilem1  15882  sin0pilem2  15883  mpodvdsmulf1o  16104  mersenne  16111  perfectlem2  16114  lgsval2lem  16129  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1f1o  16179  gausslemma2dlem2  16181  gausslemma2dlem3  16182  lgsquadlemofi  16195  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1a1  16205  2sqlem6  16239  2sqlem8  16242  2sqlem10  16244  usgruspgrben  16427  uspgredg2v  16462  usgredg2v  16465  subuhgr  16513  subupgr  16514  subumgr  16515  subusgr  16516  vtxedgfi  16530  vtxlpfi  16531  wlk1walkdom  16600  wlkres  16620  eupth2lembfi  16718  depindlem1  16747  depindlem2  16748  depindlem3  16749  dichmul0or  16760  fnmptd  16832  bj-charfun  16833  bj-charfundc  16834  bj-charfunr  16836  pw1nct  17033  wexmiddiffi  17044  nnsf  17048  nninfalllem1  17051  nninfall  17052  nninfself  17056  nninfsellemeq  17057  nninfsellemeqinf  17059  nninfsel  17060  nnnninfex  17065  nninfnfiinf  17066  repiecef  17077  isomninnlem  17079  trilpolemeq1  17089  trilpo  17092  apdiff  17097  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  redcwlpo  17105  redc0  17107  reap0  17108  dceqnconst  17110  dcapnconst  17111  nconstwlpolem  17115  nconstwlpo  17116  neapmkv  17118  ltlenmkv  17120