Theorem mpteq2dv 4534

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

Hypothesis

Ref	Expression
mpteq2dv.1	|- ( ph -> B = C )

Assertion

Ref	Expression
mpteq2dv	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)

Proof of Theorem mpteq2dv

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3 |- ( ph -> B = C )
2	1	adantr 465	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	2	mpteq2dva 4533	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   |-> cmpt 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507

This theorem is referenced by:  ofeq  6526  mpt2curryvald  6999  rdgeq1  7077  rdgeq2  7078  omv  7162  oev  7164  oieq1  7937  oieq2  7938  cantnffvalOLD  8082  cantnflem1  8108  cantnflem1OLD  8131  wunex2  9116  wuncval2  9125  reexALT  11214  seqof2  12133  limsupval  13260  sumeq2w  13477  sumeq2ii  13478  cbvsum  13480  summo  13502  fsum  13505  fsumrlim  13588  fsumo1  13589  rpnnen2lem1  13809  rpnnen2lem2  13810  rpnnen  13821  1arithlem1  14300  vdwapval  14350  vdwlem6  14363  vdwlem8  14365  vdwlem9  14366  vdwlem10  14367  ramub1lem2  14404  ramcl  14406  prdsplusgval  14728  prdsmulrval  14730  prdsdsval  14733  prdsvscaval  14734  ismon  14989  fucco  15189  curf1  15352  curf2  15356  yonedalem4a  15402  grplactfval  15946  galactghm  16233  pmtrval  16282  sylow1  16429  sylow2b  16449  sylow3lem5  16457  sylow3  16459  iscyg  16685  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzmhm  16760  gsumzmhmOLD  16761  ablfac2  16942  gsumdixpOLD  17058  gsumdixp  17059  fczpsrbag  17815  psrmulfval  17837  mvrval  17876  subrgmvr  17922  mplcoe1  17926  mplcoe3  17927  mplcoe3OLD  17928  mplcoe5  17930  mplcoe2OLD  17932  mplmon2  17957  subrgascl  17962  evlslem2  17979  evlslem3  17982  evlslem1  17983  mpfrcl  17986  evlsval  17987  evlsvar  17991  mpfind  18004  coe1fval  18043  pf1ind  18190  evl1gsumadd  18193  zncyg  18382  phllmhm  18462  isphld  18484  frlmgsumOLD  18596  frlmgsum  18597  frlmipval  18605  frlmphl  18607  uvcval  18611  mamuval  18683  mamufv  18684  matgsum  18734  madetsumid  18758  mat1dimmul  18773  mvmulval  18840  mvmulfv  18841  mavmulfv  18843  1mavmul  18845  marepvval0  18863  mulmarep1gsum1  18870  mdetleib  18884  mdetleib2  18885  mdetfval1  18887  mdetleib1  18888  mdet0pr  18889  m1detdiag  18894  mdetralt  18905  mdetunilem9  18917  m2detleib  18928  smadiadetlem3  18965  mat2pmatmul  19027  decpmatmul  19068  decpmatmulsumfsupp  19069  pmatcollpw1  19072  monmatcollpw  19075  pmatcollpw3lem  19079  pmatcollpw3fi1lem2  19083  pm2mpval  19091  pm2mpfval  19092  mply1topmatval  19100  mp2pm2mplem1  19102  mp2pm2mplem3  19104  ptbasfi  19845  ptcnplem  19885  ptrescn  19903  cnmpt2k  19952  xkohmeo  20079  fmval  20207  fmf  20209  ptcmpg  20320  tmdmulg  20354  prdstmdd  20385  tsmspropd  20393  prdsxmslem2  20795  metdsval  21114  fsumcn  21137  expcn  21139  lebnumlem3  21226  pcoval  21274  pi1xfrcnv  21320  rrxds  21588  rrxmval  21595  itg11  21861  mbfi1fseqlem2  21886  mbfi1fseqlem6  21890  mbfi1fseq  21891  mbfi1flimlem  21892  mbfmullem  21895  itg2const  21910  itg2mulc  21917  itg2monolem1  21920  itg2i1fseqle  21924  itg2i1fseq  21925  itg2addlem  21928  itg2cnlem1  21931  itg2cn  21933  isibl  21935  isibl2  21936  iblitg  21938  itgz  21950  itgvallem  21954  itgvallem3  21955  iblcnlem1  21957  itgcnlem  21959  iblrelem  21960  iblposlem  21961  iblpos  21962  itgrevallem1  21964  itgposval  21965  iblss2  21975  itgss  21981  itgfsum  21996  iblabslem  21997  iblmulc2  22000  bddmulibl  22008  itgcn  22012  ellimc  22040  dvnfval  22088  cpnfval  22098  dvexp  22119  dvexp2  22120  dvmptfsum  22139  dvlipcn  22158  dvivthlem1  22172  dvfsumle  22185  dvfsumabs  22187  dvfsumlem2  22191  elply2  22356  elplyr  22361  elplyd  22362  coeeu  22385  coelem  22386  coeeq  22387  plyco  22401  coe11  22412  coe1termlem  22417  dgrcolem1  22432  dvply2g  22443  elqaalem3  22479  eltayl  22517  tayl0  22519  taylthlem1  22530  taylthlem2  22531  ulmcau  22552  ulmdvlem1  22557  ulmdvlem3  22559  mtest  22561  mtestbdd  22562  pserval  22567  pserulm  22579  psercn  22583  pserdvlem2  22585  abelthlem3  22590  logtayl  22797  dvcxp1  22872  dmarea  23043  musum  23223  dchrptlem2  23296  dchrptlem3  23297  dchrpt  23298  lgsval  23331  lgsval4lem  23338  lgsneg  23350  lgsmod  23352  rpvmasum2  23453  padicfval  23557  ostth2  23578  ostth3  23579  ostth  23580  lmif  23856  islmib  23858  wwlkn  24386  clwwlkn  24471  clwwlknprop  24476  htthlem  25538  htth  25539  pjhfval  26018  hosmval  26358  hommval  26359  hodmval  26360  hfsmval  26361  hfmmval  26362  brafval  26566  kbfval  26575  indval  27695  ofceq  27764  itgeq12dv  27936  ballotlemfval  28096  lgamgulmlem2  28240  lgamgulmlem5  28243  ptpcon  28346  cvmliftlem15  28411  cvmlift2lem4  28419  cvmlift2  28429  snmlval  28444  snmlflim  28445  relexp0  28555  relexpsucr  28556  prodeq2w  28649  prodmo  28673  fprod  28678  faclim  28776  faclim2  28778  trpredeq1  28908  trpredeq2  28909  bpolylem  29415  voliunnfl  29663  itg2addnclem  29671  itg2addnclem3  29673  itg2addnc  29674  itg2gt0cn  29675  iblabsnclem  29683  iblmulc2nc  29685  ftc1anclem2  29696  ftc1anclem6  29700  ftc1anclem8  29702  ftc1anc  29703  ftc2nc  29704  dvcncxp1  29705  upixp  29851  rrncmslem  29959  ismrer1  29965  mzpclval  30289  mzpcl2  30294  mzpexpmpt  30309  mzpsubst  30313  mzpcompact2lem  30316  rmxfval  30472  rmyfval  30473  aomclem8  30639  hbtlem1  30704  hbtlem7  30706  itgpowd  30815  expgrowthi  30866  expgrowth  30868  addrval  30981  subrval  30982  mulvval  30983  fmulcl  31159  fmuldfeqlem1  31160  stoweidlem2  31330  stoweidlem17  31345  stoweidlem19  31347  stoweidlem20  31348  stoweidlem43  31371  stoweidlem62  31390  stoweid  31391  fourierdlem112  31547  fourierdlem113  31548  lincop  32108  tendoplcbv  35589  tendopl  35590  tendoicbv  35607  tendoi  35608  dihfval  36046  lcfl7N  36316  lcfrlem8  36364  lcfrlem9  36365  lcf1o  36366  hvmapval  36575  hdmap1fval  36612  hdmapffval  36644  hdmapfval  36645  hgmapffval  36703  hgmapfval  36704