Theorem fvmptd 5961

Description: Deduction version of fvmpt 5956. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
fvmptd.1
fvmptd.2
fvmptd.3
fvmptd.4

Assertion

Ref	Expression
fvmptd

Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem fvmptd

Step	Hyp	Ref	Expression
1		fvmptd.1	. . 3
2	1	fveq1d 5873	. 2
3		fvmptd.3	. . 3
4		fvmptd.2	. . . . 5
5	3, 4	csbied 3461	. . . 4
6		fvmptd.4	. . . 4
7	5, 6	eqeltrd 2545	. . 3
8		eqid 2457	. . . 4
9	8	fvmpts 5958	. . 3
10	3, 7, 9	syl2anc 661	. 2
11	2, 10, 5	3eqtrd 2502	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  [_csb 3434  e.cmpt 4510  `cfv 5593

This theorem is referenced by:  fvmptdv2  5969  mpt2curryvald  7018  ttukeylem3  8912  ccatval1  12595  ccatval2  12596  repswsymb  12746  prdsvscafval  14877  mrcval  15007  cidval  15074  subcid  15216  idfu2nd  15246  resf2nd  15264  fuccoval  15332  fucid  15340  homaval  15358  idaval  15385  setcval  15404  setcid  15413  catcval  15423  catcid  15430  prf1  15469  prf2  15471  curf1  15494  curf11  15495  curf2val  15499  hofval  15521  hof2  15526  yonval  15530  yonedalem4a  15544  frmdval  16019  vrmdval  16025  pmtrdifwrdellem3  16508  gexval  16598  pj1val  16713  dpjval  17105  sraval  17822  opsrval  18139  cply1mul  18335  cply1coe0  18341  cply1coe0bi  18342  gsummoncoe1  18346  evls1sca  18360  frlmphl  18812  mat1rhmval  18981  scmatrhmval  19029  mvmulfv  19046  mavmulfv  19048  mdetuni0  19123  mat2pmatval  19225  m2cpm  19242  cpm2mval  19251  m2cpminvid2lem  19255  decpmatid  19271  decpmatmullem  19272  pmatcollpw2lem  19278  monmatcollpw  19280  pmatcollpw3fi1lem1  19287  pm2mpfval  19297  mply1topmatval  19305  mp2pm2mplem1  19307  mp2pm2mplem4  19310  pm2mpmhmlem2  19320  chpmatval  19332  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  lmfval  19733  kgenval  20036  ptval  20071  fcfval  20534  cnextfval  20562  ustval  20705  utopval  20735  ustuqtoplem  20742  utopsnneiplem  20750  tusval  20769  blfvalps  20886  tmsval  20984  metuvalOLD  21052  metuval  21053  caufval  21714  rrxmvallem  21831  rrxmval  21832  taylpval  22762  efgh  22928  logexprlim  23500  dchrval  23509  dchr1  23532  mirval  24036  mirfv  24037  israg  24074  perpln1  24087  perpln2  24088  isperp  24089  ishpg  24128  midf  24142  ismidb  24144  lmif  24151  islmib  24153  edgval  24339  wlkiswwlk2lem2  24692  clwlkisclwwlklem2fv1  24782  clwlkisclwwlklem2fv2  24783  sgnsval  27718  metidval  27869  pstmval  27874  qqhvval  27964  indv  28026  indval  28027  indfval  28030  esummulc1  28087  esumcvg  28092  ofcval  28098  sigagenval  28140  measinb  28192  omsval  28264  omsfval  28265  sitgfval  28283  eulerpartlemsv1  28295  eulerpartlems  28299  eulerpartlemgvv  28315  fibp1  28340  totprobd  28365  probmeasb  28369  cndprobval  28372  dstrvprob  28410  dstfrvinc  28415  dstfrvclim1  28416  ballotlemfval  28428  ballotlemsv  28448  gsumnunsn  28493  signsply0  28508  signstfval  28521  afsval  28551  lgamgulmlem2  28572  lgamcvglem  28582  cvmliftlem9  28738  mvrsval  28865  mrsubfval  28868  mrsubval  28869  msubfval  28884  msubval  28885  msrval  28898  relexp0  29052  relexpsucr  29053  rtrclreclem.subset  29068  rtrclreclem.min  29070  dfrtrcl2  29071  mblfinlem2  30052  areacirc  30112  itgpowd  31182  dvgrat  31193  radcnvrat  31195  hashnzfzclim  31227  binomcxplemnn0  31254  binomcxplemrat  31255  binomcxplemfrat  31256  binomcxplemradcnv  31257  binomcxplemcvg  31259  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  fmuldfeqlem1  31576  clim1fr1  31607  climrec  31609  climexp  31611  climneg  31616  mullimcf  31629  divcnvg  31633  sumnnodd  31636  expfac  31663  cncfshift  31676  icccncfext  31690  cncfioobdlem  31699  dvsinax  31708  fperdvper  31715  dvcosax  31723  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  itgsinexp  31753  itgcoscmulx  31768  itgsincmulx  31773  itgsubsticclem  31774  itgsubsticc  31775  itgiccshift  31779  stoweidlem7  31789  stoweidlem17  31799  stoweidlem32  31814  stoweidlem34  31816  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem1  31856  stirlinglem2  31857  stirlinglem3  31858  stirlinglem4  31859  stirlinglem5  31860  stirlinglem7  31862  stirlinglem8  31863  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  dirkerval2  31876  dirkercncflem2  31886  fourierdlem7  31896  fourierdlem13  31902  fourierdlem14  31903  fourierdlem16  31905  fourierdlem18  31907  fourierdlem19  31908  fourierdlem21  31910  fourierdlem22  31911  fourierdlem26  31915  fourierdlem37  31926  fourierdlem39  31928  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem53  31942  fourierdlem62  31951  fourierdlem63  31952  fourierdlem65  31954  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem83  31972  fourierdlem84  31973  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem93  31982  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fouriersw  32014  elaa2lem  32016  etransclem1  32018  etransclem12  32029  etransclem13  32030  etransclem17  32034  etransclem18  32035  etransclem21  32038  etransclem27  32044  etransclem31  32048  etransclem32  32049  etransclem33  32050  etransclem35  32052  etransclem46  32063  etransclem48  32065  vtxval  32383  gordval  32388  gsizval  32389  clintopval  32528  assintopval  32529  isofval  32566  isofn  32567  cicfval  32581  initoval  32603  termoval  32604  zerooval  32605  estrcval  32630  estrcid  32640  funcestrcsetclem1  32646  funcsetcestrclem1  32660  c0mgm  32715  c0mhm  32716  c0snmgmhm  32720  c0snmhm  32721  zrrnghm  32723  rngcvalOLD  32769  rngcval  32770  rngcidOLD  32799  zrinitorngc  32808  zrtermorngc  32809  ringcvalOLD  32815  ringcval  32816  funcringcsetcOLD2lem1  32844  ringcidOLD  32862  funcringcsetclem1OLD  32867  zrtermoringc  32878  rhmsubcOLDlem3  32915  scmsuppss  32965  ply1mulgsum  32990  lincop  33009  lincext3  33057  lindslinindsimp1  33058  lindsrng01  33069  lincresunit2  33079  lincresunit3lem1  33080  islindeps2  33084  bj-finsumval0  34663  cdleme31fv2  36119  tendopl2  36503  tendoi2  36521  erngplus2  36530  erngplus2-rN  36538  hlhilset  37664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fv 5601