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  4213  triun  4244  issod  4466  frirrg  4497  frind  4499  peano2  4744  dmmptd  5517  fun11iun  5663  fniinfv  5764  eqfnfv  5809  eqfnfvd  5812  fnmptfvd  5816  dff3im  5856  dffo4  5859  fmptd  5865  ffnfv  5869  fmpt2d  5873  ffvresb  5874  funiun  5893  fconst2g  5933  fconstfvm  5936  resfunexg  5939  eufnfv  5952  foco2  5962  fniunfv  5971  fcofo  5993  fliftel  6002  fliftfun  6005  fliftfuns  6007  riota5f  6068  f1ocnvd  6295  f1o3d  6301  suppssov1  6302  offval2  6322  ofrfval2  6323  offveqb  6326  offveq  6327  caofref  6331  caofinvl  6332  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  opabex3d  6354  uchoice  6375  oprssdmm  6409  f1od2  6475  disjxp1  6476  funsssuppss  6502  suppofss1dcl  6508  suppofss2dcl  6509  tfrlem1  6584  tfrlemisucaccv  6601  tfrlemiubacc  6606  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemubacc  6622  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemubacc  6635  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  rdgon  6662  freccllem  6678  frecfcllem  6680  omcl  6739  oeicl  6740  qliftfuns  6898  ixpeq2dva  7001  xpf1o  7150  mapxpen  7154  isinfinf  7207  fimax2gtrilemstep  7211  undifdcss  7236  opabfi  7253  fissfi  7269  relresfin  7270  funisfsuppdc  7298  fdcf1  7321  f1setfi  7322  2omap  7324  eqsuptid  7343  eqinftid  7367  difinfsnlem  7445  difinfsn  7446  ctmlemr  7454  ctm  7455  ctssdclemn0  7456  ctssdccl  7457  enumctlemm  7460  nninfninc  7469  nnnninf  7472  nnnninfeq  7474  enomnilem  7484  ismkvnex  7501  enmkvlem  7507  enwomnilem  7515  nninfwlporlemd  7518  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  nninfwlpoim  7525  nninfinfwlpo  7526  finacn  7566  acfun  7569  exmidaclem  7570  exmidontriimlem4  7586  exmidontriim  7587  pw1on  7591  ccfunen  7636  cc2lem  7638  cc3  7640  acnccim  7644  genprndl  7894  genprndu  7895  nqprloc  7918  ltexprlemrnd  7978  ltexprlemdisj  7979  lteupri  7990  recexprlemrnd  8002  recexprlemdisj  8003  caucvgprlemlim  8054  caucvgprprlemlim  8084  suplocexprlemml  8089  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  caucvgsrlembound  8167  caucvgsrlemgt1  8168  caucvgsrlemoffgt1  8172  caucvgsr  8175  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  elrealeu  8202  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  negeu  8524  eqord1  8818  eqord2  8819  creur  9297  creui  9298  suprzclex  9754  supinfneg  10010  infsupneg  10011  infregelbex  10013  indstr2  10024  irraddap  10062  iooidg  10327  iccsupr  10384  icoshftf1o  10409  fznlem  10461  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  suprzubdc  10687  zsupssdc  10689  exbtwnzlemstep  10698  exbtwnzlemex  10700  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgtcl  10869  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  frecuzrdgfunlem  10876  frecuzrdgsuctlem  10880  nninfinf  10900  iseqovex  10915  seq3val  10917  seqvalcd  10918  seq3-1  10919  seqf  10921  seq3p1  10922  seqovcd  10924  seqp1cd  10927  seq3clss  10928  seq3fveq2  10932  seqfveq2g  10934  seqfveqg  10935  seq3fveq  10936  seq3feq  10937  seq3shft2  10938  seqshft2g  10939  monoord  10942  monoord2  10943  ser3mono  10944  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemqk  10964  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  seqf1og  10978  seq3id3  10981  seq3id  10982  seq3id2  10983  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  ser3ge0  10993  nn0ltexp2  11168  bccl  11226  hashinfuni  11237  hashennnuni  11239  sshashneg  11302  hashfibclem  11303  hashf1lem1  11306  wrdexg  11336  ccatlen  11384  ccatvalfn  11390  ccatrn  11398  swrdlen  11445  swrdwrdsymbg  11457  swrdswrd  11498  wrdind  11515  reuccatpfxs1  11540  shftf  11616  seq3shft  11624  caucvgrelemcau  11767  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemcvg  11806  resqrexlemglsq  11809  resqrexlemga  11810  maxabslemval  11996  negfi  12016  minmax  12019  xrmaxiflemval  12040  xrminmax  12055  climconst  12080  2clim  12091  climcn1  12098  climcn2  12099  reccn2ap  12103  cn1lem  12104  climsqz  12125  climsqz2  12126  climcau  12137  climrecvg1n  12138  serf0  12142  sumeq2dv  12158  sumrbdclem  12168  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  zsumdc  12175  isum  12176  fsumgcl  12177  fsum3  12178  fsumf1o  12181  isumss  12182  fisumss  12183  isumss2  12184  fsum3cvg2  12185  fsumsersdc  12186  fsum3ser  12188  fsumcl2lem  12189  fsumadd  12197  fsumsplit  12198  fsumm1  12207  fsum1p  12209  isumclim3  12214  isummulc2  12217  sumsplitdc  12223  fsum2dlemstep  12225  fisumcom2  12229  fsumshftm  12236  fsummulc2  12239  fsumge1  12252  fsum00  12253  fsumabs  12256  telfsumo  12257  telfsumo2  12258  fsumparts  12261  fsumrelem  12262  fsumiun  12268  hashiun  12269  hash2iun  12270  binomlem  12274  isumshft  12281  isum1p  12283  isumnn0nn  12284  isumrpcl  12285  isumlessdc  12287  divcnv  12288  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemseq  12317  cvgratnnlemabsle  12318  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratnn  12322  cvgratz  12323  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  clim2prod  12330  prodeq2dv  12357  prodrbdclem  12362  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  iprodap  12371  fprodseq  12374  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodmul  12382  fprodsplit  12388  fprodm1  12389  fprod1p  12390  fprodm1s  12392  fprodp1s  12393  fprodunsn  12395  fprodcl2lem  12396  fprodabs  12407  fprodeq0  12408  fprodap0  12412  fprod2dlemstep  12413  fprodcom2fi  12417  fprodrec  12420  fprodmodd  12432  efcvgfsum  12458  dvdsssfz1  12643  bitsfi  12748  bitsinv1  12753  dvdsbnd  12757  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemle  12809  bezoutlemsup  12810  dfgcd3  12811  dfgcd2  12815  nnwodc  12837  uzwodc  12838  nnwosdc  12840  nninfctlemfo  12841  coprmgcdb  12890  prmdc  12932  isprm5  12945  isprm6  12950  phivalfi  13018  phibndlem  13022  dfphi2  13026  hashdvds  13027  phiprmpw  13028  phimullem  13031  eulerthlemfi  13034  dvdsfi  13045  hashgcdeq  13046  phisum  13047  reumodprminv  13060  pclemdc  13095  pc2dvds  13137  pcz  13139  pcprmpw2  13140  pcmptdvds  13152  pcprod  13153  pcfac  13157  qexpz  13159  prmpwdvds  13162  pockthg  13164  infpnlem2  13167  1arithlem4  13173  1arith  13174  4sqlemafi  13202  4sqlemffi  13203  4sqleminfi  13204  ballotfilemcinfi  13281  ballotfilemdifcfi  13282  ballotfilemcinfz  13283  ballotfilemdifcfz  13284  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemefi  13294  ballotfilemodife  13297  ballotfilemiex  13301  ennnfonelemex  13362  ennnfonelemfun  13365  ennnfonelemf1  13366  ennnfonelemnn0  13370  ennnfonelemim  13372  exmidunben  13374  ctinfomlemom  13375  ctinfom  13376  ctinf  13378  ctiunctlemudc  13385  ctiunctlemf  13386  ctiunctlemfo  13387  omctfn  13391  ssnnctlemct  13394  nninfdclemcl  13396  nninfdclemp1  13398  imasival  13685  ismgmid2  13758  mgmidsssn0  13762  grpinvalem  13763  grpinva  13764  gzsumress  13770  issgrpd  13785  sgrpidmndm  13791  ismndd  13808  mndpfo  13809  mhmima  13856  mhmeql  13857  gsumvallem2  13858  isgrpd2e  13883  dfgrp2  13890  grpidd2  13904  isgrpinv  13917  grplrinv  13920  grpidinv  13922  dfgrp3me  13963  mhmmnd  13977  ghmgrp  13979  mulgsubcl  13997  issubg2m  14050  issubgrpd2  14051  grpissubg  14055  subgintm  14059  nmzsubg  14071  ssnmz  14072  ghmrn  14118  ghmeql  14128  ghmf1  14134  conjnmz  14140  conjnmzb  14141  cntzsgrpcl  14166  cntz2ss  14167  cntzsubm  14169  cntzsubg  14170  cntzmhm  14172  cntzmhm2  14173  rinvmod  14202  gsummptfidmadd  14250  gsummptfidmsplit  14253  idjufi  14268  idjusnfi  14269  gsum2dfilem2  14271  gsum2dfi  14272  gsum2d2fi  14273  prdsplusgsgrpcl  14296  prdsplusgcl  14298  prdsidlem  14299  prdsinvlem  14302  pwsbas  14311  srgrz  14394  srglz  14395  srgisid  14396  ringsrg  14458  rhmdvdsr  14590  rhmopp  14591  subrngintm  14628  subrg1  14647  subrgugrp  14656  subrgintm  14659  rrgsupp  14682  unitrrg  14684  aprap  14706  islmodd  14737  lssuni  14808  lsssubg  14822  lssintclm  14829  dflidl2rng  14926  lidlsubg  14931  cnsubglem  15024  gsumfsum  15031  znf1o  15094  znidomb  15101  asclfnd  15131  psrbagfi  15166  psrbagdceq  15167  psrbaglecl  15172  psrbagcon  15174  psrbaglefifi  15175  psrbagmaxlem1  15178  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  psr1clfi  15207  psrlidmfi  15208  psrridmfi  15209  mplsubgfi  15234  fiinbas  15292  tgclb  15308  restbasg  15411  iscnp4  15461  cnco  15464  cnptopco  15465  cnss1  15469  cnss2  15470  cncnpi  15471  cncnp  15473  cnconst2  15476  cnrest  15478  cnptopresti  15481  cnpdis  15485  lmtopcnp  15493  txbasval  15510  tx1cn  15512  tx2cn  15513  txcnp  15514  upxp  15515  txdis1cn  15521  cnmpt11  15526  psmet0  15570  psmettri2  15571  psmetxrge0  15575  psmetres2  15576  ismeti  15589  xmetpsmet  15612  blsscls2  15736  comet  15742  xmettx  15753  tgioo  15797  tgqioo  15798  fsumcncntop  15810  elcncf1di  15822  cdivcncfap  15847  mulcncflem  15850  mulcncf  15851  cnopnap  15854  divcncfap  15857  dedekindeulemuub  15860  dedekindeulemlu  15864  suplociccreex  15867  suplociccex  15868  dedekindicclemuub  15869  dedekindicclemlu  15873  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemdisj  15883  ivthinclemloc  15884  ivthinc  15886  ivthdec  15887  dich0  15895  ivthdich  15896  cnplimclemr  15912  limccnp2cntop  15920  limccoap  15921  dvcn  15943  dvfre  15953  dvrecap  15956  dvmptclx  15961  dvmptaddx  15962  dvmptmulx  15963  dveflem  15969  dvef  15970  ply1termlem  15985  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  plycj  16004  plyreres  16007  dvply1  16008  sin0pilem1  16025  sin0pilem2  16026  zprmlogbaplem2  16233  ppiqfi  16259  prmdvdsfi  16260  ppiprm  16276  chtprm  16278  chtdif  16281  efchtqdvds  16282  ppidif  16286  prmorcht  16299  mpodvdsmulf1o  16301  ppiqub  16310  chtublem  16312  mersenne  16314  perfectlem2  16317  bposlem1  16328  bposlem3  16330  bposlem5  16332  bposlem6  16333  lgsval2lem  16351  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1f1o  16401  gausslemma2dlem2  16403  gausslemma2dlem3  16404  lgsquadlemofi  16417  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem1a1  16427  2sqlem6  16461  2sqlem8  16464  2sqlem10  16466  usgruspgrben  16649  uspgredg2v  16684  usgredg2v  16687  subuhgr  16735  subupgr  16736  subumgr  16737  subusgr  16738  vtxedgfi  16752  vtxlpfi  16753  wlk1walkdom  16822  wlkres  16842  eupth2lembfi  16940  depindlem1  16969  depindlem2  16970  depindlem3  16971  dichmul0or  16982  fnmptd  17054  bj-charfun  17055  bj-charfundc  17056  bj-charfunr  17058  pw1nct  17255  wexmiddiffi  17266  nnsf  17271  nninfalllem1  17274  nninfall  17275  nninfself  17279  nninfsellemeq  17280  nninfsellemeqinf  17282  nninfsel  17283  nnnninfex  17288  nninfnfiinf  17289  repiecef  17300  isomninnlem  17302  trilpolemeq1  17313  trilpo  17316  apdiff  17321  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  redcwlpo  17329  redc0  17331  reap0  17332  dceqnconst  17334  dcapnconst  17335  nconstwlpolem  17339  nconstwlpo  17340  neapmkv  17342  ltlenmkv  17344