Theorem mpteq2dv 4539

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)

Hypothesis

Ref	Expression
mpteq2dv.1

Assertion

Ref	Expression
mpteq2dv

Distinct variable group:   ,

Proof of Theorem mpteq2dv

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3
2	1	adantr 465	. 2
3	2	mpteq2dva 4538	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  e.cmpt 4510

This theorem is referenced by:  ofeq  6542  mpt2curryvald  7018  rdgeq1  7096  rdgeq2  7097  omv  7181  oev  7183  oieq1  7958  oieq2  7959  cantnffvalOLD  8103  cantnflem1  8129  cantnflem1OLD  8152  wunex2  9137  wuncval2  9146  reexALT  11243  seqof2  12165  limsupval  13297  sumeq2w  13514  sumeq2ii  13515  cbvsum  13517  summo  13539  fsum  13542  fsumrlim  13625  fsumo1  13626  prodeq2w  13719  prodmo  13743  fprod  13748  rpnnen2lem1  13948  rpnnen2lem2  13949  rpnnen  13960  1arithlem1  14441  vdwapval  14491  vdwlem6  14504  vdwlem8  14506  vdwlem9  14507  vdwlem10  14508  ramub1lem2  14545  ramcl  14547  prdsplusgval  14870  prdsmulrval  14872  prdsdsval  14875  prdsvscaval  14876  ismon  15128  fucco  15331  curf1  15494  curf2  15498  yonedalem4a  15544  grplactfval  16136  galactghm  16428  pmtrval  16476  sylow1  16623  sylow2b  16643  sylow3lem5  16651  sylow3  16653  iscyg  16882  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumzmhm  16957  gsumzmhmOLD  16958  ablfac2  17140  gsumdixpOLD  17257  gsumdixp  17258  fczpsrbag  18016  psrmulfval  18038  mvrval  18077  subrgmvr  18123  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  mplmon2  18158  subrgascl  18163  evlslem2  18180  evlslem3  18183  evlslem1  18184  mpfrcl  18187  evlsval  18188  evlsvar  18192  mpfind  18205  coe1fval  18244  pf1ind  18391  evl1gsumadd  18394  zncyg  18587  phllmhm  18667  isphld  18689  frlmgsumOLD  18801  frlmgsum  18802  frlmipval  18810  frlmphl  18812  uvcval  18816  mamuval  18888  mamufv  18889  matgsum  18939  madetsumid  18963  mat1dimmul  18978  mvmulval  19045  mvmulfv  19046  mavmulfv  19048  1mavmul  19050  marepvval0  19068  mulmarep1gsum1  19075  mdetleib  19089  mdetleib2  19090  mdetfval1  19092  mdetleib1  19093  mdet0pr  19094  m1detdiag  19099  mdetralt  19110  mdetunilem9  19122  m2detleib  19133  smadiadetlem3  19170  mat2pmatmul  19232  decpmatmul  19273  decpmatmulsumfsupp  19274  pmatcollpw1  19277  monmatcollpw  19280  pmatcollpw3lem  19284  pmatcollpw3fi1lem2  19288  pm2mpval  19296  pm2mpfval  19297  mply1topmatval  19305  mp2pm2mplem1  19307  mp2pm2mplem3  19309  ptbasfi  20082  ptcnplem  20122  ptrescn  20140  cnmpt2k  20189  xkohmeo  20316  fmval  20444  fmf  20446  ptcmpg  20557  tmdmulg  20591  prdstmdd  20622  tsmspropd  20630  prdsxmslem2  21032  metdsval  21351  fsumcn  21374  expcn  21376  lebnumlem3  21463  pcoval  21511  pi1xfrcnv  21557  rrxds  21825  rrxmval  21832  itg11  22098  mbfi1fseqlem2  22123  mbfi1fseqlem6  22127  mbfi1fseq  22128  mbfi1flimlem  22129  mbfmullem  22132  itg2const  22147  itg2mulc  22154  itg2monolem1  22157  itg2i1fseqle  22161  itg2i1fseq  22162  itg2addlem  22165  itg2cnlem1  22168  itg2cn  22170  isibl  22172  isibl2  22173  iblitg  22175  itgz  22187  itgvallem  22191  itgvallem3  22192  iblcnlem1  22194  itgcnlem  22196  iblrelem  22197  iblposlem  22198  iblpos  22199  itgrevallem1  22201  itgposval  22202  iblss2  22212  itgss  22218  itgfsum  22233  iblabslem  22234  iblmulc2  22237  bddmulibl  22245  itgcn  22249  ellimc  22277  dvnfval  22325  cpnfval  22335  dvexp  22356  dvexp2  22357  dvmptfsum  22376  dvlipcn  22395  dvivthlem1  22409  dvfsumle  22422  dvfsumabs  22424  dvfsumlem2  22428  elply2  22593  elplyr  22598  elplyd  22599  coeeu  22622  coelem  22623  coeeq  22624  plyco  22638  coe11  22650  coe1termlem  22655  dgrcolem1  22670  dvply2g  22681  elqaalem3  22717  eltayl  22755  tayl0  22757  taylthlem1  22768  taylthlem2  22769  ulmcau  22790  ulmdvlem1  22795  ulmdvlem3  22797  mtest  22799  mtestbdd  22800  pserval  22805  pserulm  22817  psercn  22821  pserdvlem2  22823  abelthlem3  22828  logtayl  23041  dvcxp1  23116  dmarea  23287  musum  23467  dchrptlem2  23540  dchrptlem3  23541  dchrpt  23542  lgsval  23575  lgsval4lem  23582  lgsneg  23594  lgsmod  23596  rpvmasum2  23697  padicfval  23801  ostth2  23822  ostth3  23823  ostth  23824  lmif  24151  islmib  24153  wwlkn  24682  clwwlkn  24767  clwwlknprop  24772  htthlem  25834  htth  25835  pjhfval  26314  hosmval  26654  hommval  26655  hodmval  26656  hfsmval  26657  hfmmval  26658  brafval  26862  kbfval  26871  ordtcnvNEW  27902  ordtrest2NEW  27905  xrhval  27996  indval  28027  ofceq  28096  itgeq12dv  28268  ballotlemfval  28428  lgamgulmlem2  28572  lgamgulmlem5  28575  ptpcon  28678  cvmliftlem15  28743  cvmlift2lem4  28751  cvmlift2  28761  snmlval  28776  snmlflim  28777  mrsubfval  28868  mrsubrn  28873  elmsubrn  28888  msubrn  28889  msubco  28891  relexp0  29052  relexpsucr  29053  faclim  29171  faclim2  29173  trpredeq1  29303  trpredeq2  29304  bpolylem  29810  voliunnfl  30058  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  iblabsnclem  30078  iblmulc2nc  30080  ftc1anclem2  30091  ftc1anclem6  30095  ftc1anclem8  30097  ftc1anc  30098  ftc2nc  30099  dvcncxp1  30100  upixp  30220  rrncmslem  30328  ismrer1  30334  mzpclval  30657  mzpcl2  30662  mzpexpmpt  30677  mzpsubst  30681  mzpcompact2lem  30684  rmxfval  30840  rmyfval  30841  aomclem8  31007  hbtlem1  31072  hbtlem7  31074  itgpowd  31182  expgrowthi  31238  expgrowth  31240  binomcxplemdvsum  31260  addrval  31375  subrval  31376  mulvval  31377  fmulcl  31575  fmuldfeqlem1  31576  fprodcncf  31704  dvnmptdivc  31735  dvnxpaek  31739  dvnmul  31740  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  dvnprod  31746  stoweidlem2  31784  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem43  31825  stoweidlem62  31844  stoweid  31845  dirkercncflem2  31886  fourierdlem112  32001  fourierdlem113  32002  etransclem1  32018  etransclem5  32022  etransclem17  32034  etransclem19  32036  etransclem22  32039  c0rhm  32718  c0rnghm  32719  lincop  33009  aacllem  33216  tendoplcbv  36501  tendopl  36502  tendoicbv  36519  tendoi  36520  dihfval  36958  lcfl7N  37228  lcfrlem8  37276  lcfrlem9  37277  lcf1o  37278  hvmapval  37487  hdmap1fval  37524  hdmapffval  37556  hdmapfval  37557  hgmapffval  37615  hgmapfval  37616

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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4511  df-mpt 4512