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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

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

This theorem is referenced by:  ralrimivvva  2633  rgen2  2636  rgen3  2637  nrexdv  2643  r19.29vva  2696  rabbidva  2809  ssrabdv  3327  ss2rabdv  3329  iuneq2dv  4028  iunssd  4053  disjeq2dv  4106  mpteq12dva  4207  triun  4237  issod  4459  frirrg  4490  frind  4492  peano2  4737  dmmptd  5509  fun11iun  5655  fniinfv  5755  eqfnfv  5797  eqfnfvd  5800  fnmptfvd  5804  dff3im  5844  dffo4  5847  fmptd  5853  ffnfv  5857  fmpt2d  5861  ffvresb  5862  funiun  5881  fconst2g  5921  fconstfvm  5924  resfunexg  5927  eufnfv  5939  foco2  5949  fniunfv  5958  fcofo  5980  fliftel  5989  fliftfun  5992  fliftfuns  5994  riota5f  6055  f1ocnvd  6282  f1o3d  6288  suppssov1  6289  offval2  6308  ofrfval2  6309  offveqb  6312  offveq  6313  caofref  6317  caofinvl  6318  caofid0l  6319  caofid0r  6320  caofid1  6321  caofid2  6322  opabex3d  6340  uchoice  6361  oprssdmm  6395  f1od2  6461  disjxp1  6462  funsssuppss  6488  suppofss1dcl  6494  suppofss2dcl  6495  tfrlem1  6569  tfrlemisucaccv  6586  tfrlemiubacc  6591  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemubacc  6607  tfr1onlemaccex  6609  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemubacc  6620  tfrcllemaccex  6622  tfrcllemres  6623  tfrcl  6625  rdgon  6647  freccllem  6663  frecfcllem  6665  omcl  6724  oeicl  6725  qliftfuns  6883  ixpeq2dva  6985  xpf1o  7134  mapxpen  7138  isinfinf  7191  fimax2gtrilemstep  7195  undifdcss  7220  opabfi  7237  fissfi  7253  fdcf1  7306  f1setfi  7307  2omap  7308  eqsuptid  7327  eqinftid  7351  difinfsnlem  7429  difinfsn  7430  ctmlemr  7438  ctm  7439  ctssdclemn0  7440  ctssdccl  7441  enumctlemm  7444  nninfninc  7453  nnnninf  7456  nnnninfeq  7458  enomnilem  7468  ismkvnex  7485  enmkvlem  7491  enwomnilem  7499  nninfwlporlemd  7502  nninfwlpoimlemg  7505  nninfwlpoimlemginf  7506  nninfwlpoim  7509  nninfinfwlpo  7510  finacn  7550  acfun  7553  exmidaclem  7554  exmidontriimlem4  7570  exmidontriim  7571  pw1on  7575  ccfunen  7620  cc2lem  7622  cc3  7624  acnccim  7628  genprndl  7878  genprndu  7879  nqprloc  7902  ltexprlemrnd  7962  ltexprlemdisj  7963  lteupri  7974  recexprlemrnd  7986  recexprlemdisj  7987  caucvgprlemlim  8038  caucvgprprlemlim  8068  suplocexprlemml  8073  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  caucvgsrlembound  8151  caucvgsrlemgt1  8152  caucvgsrlemoffgt1  8156  caucvgsr  8159  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  elrealeu  8186  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  negeu  8507  eqord1  8801  eqord2  8802  creur  9279  creui  9280  suprzclex  9723  supinfneg  9974  infsupneg  9975  infregelbex  9977  indstr2  9988  iooidg  10290  iccsupr  10347  icoshftf1o  10372  fznlem  10424  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  suprzubdc  10649  zsupssdc  10651  exbtwnzlemstep  10660  exbtwnzlemex  10662  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgtcl  10827  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgfunlem  10834  frecuzrdgsuctlem  10838  nninfinf  10858  iseqovex  10873  seq3val  10875  seqvalcd  10876  seq3-1  10877  seqf  10879  seq3p1  10880  seqovcd  10882  seqp1cd  10885  seq3clss  10886  seq3fveq2  10890  seqfveq2g  10892  seqfveqg  10893  seq3fveq  10894  seq3feq  10895  seq3shft2  10896  seqshft2g  10897  monoord  10900  monoord2  10901  ser3mono  10902  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  seq3caopr2  10908  seqcaopr2g  10909  iseqf1olemqk  10922  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seq3f1oleml  10931  seq3f1o  10932  seqf1og  10936  seq3id3  10939  seq3id  10940  seq3id2  10941  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  ser3ge0  10951  nn0ltexp2  11125  bccl  11183  hashinfuni  11194  hashennnuni  11196  sshashneg  11259  hashfibclem  11260  hashf1lem1  11263  wrdexg  11293  ccatlen  11341  ccatvalfn  11347  ccatrn  11355  swrdlen  11402  swrdwrdsymbg  11414  swrdswrd  11455  wrdind  11472  reuccatpfxs1  11497  shftf  11573  seq3shft  11581  caucvgrelemcau  11724  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemcvg  11763  resqrexlemglsq  11766  resqrexlemga  11767  maxabslemval  11952  negfi  11972  minmax  11974  xrmaxiflemval  11994  xrminmax  12009  climconst  12034  2clim  12045  climcn1  12052  climcn2  12053  reccn2ap  12057  cn1lem  12058  climsqz  12079  climsqz2  12080  climcau  12091  climrecvg1n  12092  serf0  12096  sumeq2dv  12112  sumrbdclem  12122  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  zsumdc  12129  isum  12130  fsumgcl  12131  fsum3  12132  fsumf1o  12135  isumss  12136  fisumss  12137  isumss2  12138  fsum3cvg2  12139  fsumsersdc  12140  fsum3ser  12142  fsumcl2lem  12143  fsumadd  12151  fsumsplit  12152  fsumm1  12161  fsum1p  12163  isumclim3  12168  isummulc2  12171  sumsplitdc  12177  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fsummulc2  12193  fsumge1  12206  fsum00  12207  fsumabs  12210  telfsumo  12211  telfsumo2  12212  fsumparts  12215  fsumrelem  12216  fsumiun  12222  hashiun  12223  hash2iun  12224  binomlem  12228  isumshft  12235  isum1p  12237  isumnn0nn  12238  isumrpcl  12239  isumlessdc  12241  divcnv  12242  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemseq  12271  cvgratnnlemabsle  12272  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratnn  12276  cvgratz  12277  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  clim2prod  12284  prodeq2dv  12311  prodrbdclem  12316  fproddccvg  12317  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  iprodap  12325  fprodseq  12328  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodmul  12336  fprodsplit  12342  fprodm1  12343  fprod1p  12344  fprodm1s  12346  fprodp1s  12347  fprodunsn  12349  fprodcl2lem  12350  fprodabs  12361  fprodeq0  12362  fprodap0  12366  fprod2dlemstep  12367  fprodcom2fi  12371  fprodrec  12374  fprodmodd  12386  efcvgfsum  12412  dvdsssfz1  12597  bitsfi  12702  bitsinv1  12707  dvdsbnd  12711  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemle  12763  bezoutlemsup  12764  dfgcd3  12765  dfgcd2  12769  nnwodc  12791  uzwodc  12792  nnwosdc  12794  nninfctlemfo  12795  coprmgcdb  12844  prmdc  12886  isprm5  12898  isprm6  12903  phivalfi  12968  phibndlem  12972  dfphi2  12976  hashdvds  12977  phiprmpw  12978  phimullem  12981  eulerthlemfi  12984  dvdsfi  12995  hashgcdeq  12996  phisum  12997  reumodprminv  13010  pclemdc  13045  pc2dvds  13087  pcz  13089  pcprmpw2  13090  pcmptdvds  13102  pcprod  13103  pcfac  13107  qexpz  13109  prmpwdvds  13112  pockthg  13114  infpnlem2  13117  1arithlem4  13123  1arith  13124  4sqlemafi  13152  4sqlemffi  13153  4sqleminfi  13154  ballotfilemcinfi  13202  ballotfilemdifcfi  13203  ballotfilemcinfz  13204  ballotfilemdifcfz  13205  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemefi  13215  ballotfilemodife  13218  ballotfilemiex  13222  ennnfonelemex  13283  ennnfonelemfun  13286  ennnfonelemf1  13287  ennnfonelemnn0  13291  ennnfonelemim  13293  exmidunben  13295  ctinfomlemom  13296  ctinfom  13297  ctinf  13299  ctiunctlemudc  13306  ctiunctlemf  13307  ctiunctlemfo  13308  omctfn  13312  ssnnctlemct  13315  nninfdclemcl  13317  nninfdclemp1  13319  imasival  13604  ismgmid2  13677  mgmidsssn0  13681  grpinvalem  13682  grpinva  13683  gzsumress  13689  issgrpd  13704  sgrpidmndm  13710  ismndd  13727  mndpfo  13728  mhmima  13775  mhmeql  13776  gsumvallem2  13777  isgrpd2e  13802  dfgrp2  13809  grpidd2  13823  isgrpinv  13836  grplrinv  13839  grpidinv  13841  dfgrp3me  13882  mhmmnd  13896  ghmgrp  13898  mulgsubcl  13916  issubg2m  13969  issubgrpd2  13970  grpissubg  13974  subgintm  13978  nmzsubg  13990  ssnmz  13991  ghmrn  14037  ghmeql  14047  ghmf1  14053  conjnmz  14059  conjnmzb  14060  rinvmod  14090  gsummptfidmadd  14138  prdsplusgsgrpcl  14167  prdsplusgcl  14169  prdsidlem  14170  prdsinvlem  14173  pwsbas  14182  srgrz  14262  srglz  14263  srgisid  14264  ringsrg  14325  rhmdvdsr  14455  rhmopp  14456  subrngintm  14493  subrg1  14512  subrgugrp  14521  subrgintm  14524  rrgsupp  14547  unitrrg  14549  aprap  14571  islmodd  14602  lssuni  14672  lsssubg  14686  lssintclm  14693  dflidl2rng  14790  lidlsubg  14795  cnsubglem  14888  gsumfsum  14895  znf1o  14958  znidomb  14965  psrbagfi  14982  psrbaglecl  14983  psrbagcon  14985  psr1clfi  15002  mplsubgfilemm  15012  mplsubgfilemcl  15013  mplsubgfi  15015  fiinbas  15073  tgclb  15089  restbasg  15192  iscnp4  15242  cnco  15245  cnptopco  15246  cnss1  15250  cnss2  15251  cncnpi  15252  cncnp  15254  cnconst2  15257  cnrest  15259  cnptopresti  15262  cnpdis  15266  lmtopcnp  15274  txbasval  15291  tx1cn  15293  tx2cn  15294  txcnp  15295  upxp  15296  txdis1cn  15302  cnmpt11  15307  psmet0  15351  psmettri2  15352  psmetxrge0  15356  psmetres2  15357  ismeti  15370  xmetpsmet  15393  blsscls2  15517  comet  15523  xmettx  15534  tgioo  15578  tgqioo  15579  fsumcncntop  15591  elcncf1di  15603  cdivcncfap  15628  mulcncflem  15631  mulcncf  15632  cnopnap  15635  divcncfap  15638  dedekindeulemuub  15641  dedekindeulemlu  15645  suplociccreex  15648  suplociccex  15649  dedekindicclemuub  15650  dedekindicclemlu  15654  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemdisj  15664  ivthinclemloc  15665  ivthinc  15667  ivthdec  15668  dich0  15676  ivthdich  15677  cnplimclemr  15693  limccnp2cntop  15701  limccoap  15702  dvcn  15724  dvfre  15734  dvrecap  15737  dvmptclx  15742  dvmptaddx  15743  dvmptmulx  15744  dveflem  15750  dvef  15751  ply1termlem  15766  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  plycj  15785  plyreres  15788  dvply1  15789  sin0pilem1  15805  sin0pilem2  15806  mpodvdsmulf1o  16018  mersenne  16025  perfectlem2  16028  lgsval2lem  16043  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1f1o  16093  gausslemma2dlem2  16095  gausslemma2dlem3  16096  lgsquadlemofi  16109  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1a1  16119  2sqlem6  16153  2sqlem8  16156  2sqlem10  16158  usgruspgrben  16341  uspgredg2v  16376  usgredg2v  16379  subuhgr  16427  subupgr  16428  subumgr  16429  subusgr  16430  vtxedgfi  16444  vtxlpfi  16445  wlk1walkdom  16514  wlkres  16534  eupth2lembfi  16632  depindlem1  16661  depindlem2  16662  depindlem3  16663  dichmul0or  16674  fnmptd  16746  bj-charfun  16747  bj-charfundc  16748  bj-charfunr  16750  pw1nct  16947  nnsf  16953  nninfalllem1  16956  nninfall  16957  nninfself  16961  nninfsellemeq  16962  nninfsellemeqinf  16964  nninfsel  16965  nnnninfex  16970  nninfnfiinf  16971  repiecef  16982  isomninnlem  16984  trilpolemeq1  16994  trilpo  16997  apdiff  17002  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007  redcwlpo  17010  redc0  17012  reap0  17013  dceqnconst  17015  dcapnconst  17016  nconstwlpolem  17020  nconstwlpo  17021  neapmkv  17023  ltlenmkv  17025