Theorem mpteq2dv 4513

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 466	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	2	mpteq2dva 4512	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1870   |-> cmpt 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2787  df-opab 4485  df-mpt 4486

This theorem is referenced by:  ofeq  6547  mpt2curryvald  7025  rdgeq1  7137  rdgeq2  7138  omv  7222  oev  7224  oieq1  8027  oieq2  8028  cantnflem1  8193  wunex2  9162  wuncval2  9171  reexALT  11296  seqof2  12268  relexpsucnnr  13067  relexp1g  13068  limsupval  13509  limsupvalOLD  13510  sumeq2w  13736  sumeq2ii  13737  cbvsum  13739  summo  13761  fsum  13764  fsumrlim  13849  fsumo1  13850  prodeq2w  13944  prodmo  13968  fprod  13973  bpolylem  14079  rpnnen2lem1  14245  rpnnen2lem2  14246  rpnnen  14257  1arithlem1  14830  vdwapval  14886  vdwlem6  14899  vdwlem8  14901  vdwlem9  14902  vdwlem10  14903  ramub1lem2  14948  ramcl  14950  prdsplusgval  15330  prdsmulrval  15332  prdsdsval  15335  prdsvscaval  15336  ismon  15589  fucco  15818  curf1  16061  curf2  16065  yonedalem4a  16111  grplactfval  16703  galactghm  16995  pmtrval  17043  sylow1  17190  sylow2b  17210  sylow3lem5  17218  sylow3  17220  iscyg  17449  gsumzaddlem  17489  gsumzmhm  17505  ablfac2  17657  gsumdixp  17772  fczpsrbag  18526  psrmulfval  18544  mvrval  18580  subrgmvr  18620  mplcoe1  18624  mplcoe3  18625  mplcoe5  18627  mplmon2  18651  subrgascl  18656  evlslem2  18670  evlslem3  18672  evlslem1  18673  mpfrcl  18676  evlsval  18677  evlsvar  18681  mpfind  18694  coe1fval  18733  pf1ind  18878  evl1gsumadd  18881  zncyg  19050  phllmhm  19130  isphld  19152  frlmgsum  19261  frlmipval  19268  frlmphl  19270  uvcval  19274  mamuval  19342  mamufv  19343  matgsum  19393  madetsumid  19417  mat1dimmul  19432  mvmulval  19499  mvmulfv  19500  mavmulfv  19502  1mavmul  19504  marepvval0  19522  mulmarep1gsum1  19529  mdetleib  19543  mdetleib2  19544  mdetfval1  19546  mdetleib1  19547  mdet0pr  19548  m1detdiag  19553  mdetralt  19564  mdetunilem9  19576  m2detleib  19587  smadiadetlem3  19624  mat2pmatmul  19686  decpmatmul  19727  decpmatmulsumfsupp  19728  pmatcollpw1  19731  monmatcollpw  19734  pmatcollpw3lem  19738  pmatcollpw3fi1lem2  19742  pm2mpval  19750  pm2mpfval  19751  mply1topmatval  19759  mp2pm2mplem1  19761  mp2pm2mplem3  19763  ptbasfi  20527  ptcnplem  20567  ptrescn  20585  cnmpt2k  20634  xkohmeo  20761  fmval  20889  fmf  20891  ptcmpg  21003  tmdmulg  21038  prdstmdd  21069  tsmspropd  21077  prdsxmslem2  21475  metdsval  21775  fsumcn  21798  expcn  21800  lebnumlem3  21887  pcoval  21935  pi1xfrcnv  21981  rrxds  22245  rrxmval  22252  itg11  22526  mbfi1fseqlem2  22551  mbfi1fseqlem6  22555  mbfi1fseq  22556  mbfi1flimlem  22557  mbfmullem  22560  itg2const  22575  itg2mulc  22582  itg2monolem1  22585  itg2i1fseqle  22589  itg2i1fseq  22590  itg2addlem  22593  itg2cnlem1  22596  itg2cn  22598  isibl  22600  isibl2  22601  iblitg  22603  itgz  22615  itgvallem  22619  itgvallem3  22620  iblcnlem1  22622  itgcnlem  22624  iblrelem  22625  iblposlem  22626  iblpos  22627  itgrevallem1  22629  itgposval  22630  iblss2  22640  itgss  22646  itgfsum  22661  iblabslem  22662  iblmulc2  22665  bddmulibl  22673  itgcn  22677  ellimc  22705  dvnfval  22753  cpnfval  22763  dvexp  22784  dvexp2  22785  dvmptfsum  22804  dvlipcn  22823  dvivthlem1  22837  dvfsumle  22850  dvfsumabs  22852  dvfsumlem2  22856  elply2  23018  elplyr  23023  elplyd  23024  coeeu  23047  coelem  23048  coeeq  23049  plyco  23063  coe11  23075  coe1termlem  23080  dgrcolem1  23095  dvply2g  23106  elqaalem3  23142  eltayl  23180  tayl0  23182  taylthlem1  23193  taylthlem2  23194  ulmcau  23215  ulmdvlem1  23220  ulmdvlem3  23222  mtest  23224  mtestbdd  23225  pserval  23230  pserulm  23242  psercn  23246  pserdvlem2  23248  abelthlem3  23253  logtayl  23470  dvcxp1  23545  dvcncxp1  23548  logbmpt  23590  dmarea  23748  lgamgulmlem2  23820  lgamgulmlem5  23823  musum  23983  dchrptlem2  24056  dchrptlem3  24057  dchrpt  24058  lgsval  24091  lgsval4lem  24098  lgsneg  24110  lgsmod  24112  rpvmasum2  24213  padicfval  24317  ostth2  24338  ostth3  24339  ostth  24340  lmif  24683  islmib  24685  wwlkn  25255  clwwlkn  25340  clwwlknprop  25345  htthlem  26405  htth  26406  pjhfval  26884  hosmval  27223  hommval  27224  hodmval  27225  hfsmval  27226  hfmmval  27227  brafval  27431  kbfval  27440  psgnfzto1st  28457  mdetpmtr1  28488  ordtcnvNEW  28565  ordtrest2NEW  28568  xrhval  28661  indval  28674  esum2dlem  28752  ofceq  28757  itgeq12dv  28987  ballotlemfval  29148  ptpcon  29744  cvmliftlem15  29809  cvmlift2lem4  29817  cvmlift2  29827  snmlval  29842  snmlflim  29843  mrsubfval  29934  mrsubrn  29939  elmsubrn  29954  msubrn  29955  msubco  29957  faclim  30169  faclim2  30171  trpredeq1  30248  trpredeq2  30249  poimirlem5  31648  poimirlem6  31649  poimirlem7  31650  poimirlem8  31651  poimirlem10  31653  poimirlem11  31654  poimirlem12  31655  poimirlem15  31658  poimirlem16  31659  poimirlem17  31660  poimirlem18  31661  poimirlem19  31662  poimirlem20  31663  poimirlem21  31664  poimirlem22  31665  poimirlem27  31670  voliunnfl  31687  itg2addnclem  31696  itg2addnclem3  31698  itg2addnc  31699  itg2gt0cn  31700  iblabsnclem  31708  iblmulc2nc  31710  ftc1anclem2  31721  ftc1anclem6  31725  ftc1anclem8  31727  ftc1anc  31728  ftc2nc  31729  upixp  31759  rrncmslem  31867  ismrer1  31873  tendoplcbv  34050  tendopl  34051  tendoicbv  34068  tendoi  34069  dihfval  34507  lcfl7N  34777  lcfrlem8  34825  lcfrlem9  34826  lcf1o  34827  hvmapval  35036  hdmap1fval  35073  hdmapffval  35105  hdmapfval  35106  hgmapffval  35164  hgmapfval  35165  mzpclval  35275  mzpcl2  35280  mzpexpmpt  35295  mzpsubst  35298  mzpcompact2lem  35301  rmxfval  35457  rmyfval  35458  aomclem8  35624  hbtlem1  35687  hbtlem7  35689  itgpowd  35797  expgrowthi  36318  expgrowth  36320  binomcxplemdvsum  36340  addrval  36455  subrval  36456  mulvval  36457  fmulcl  37230  fmuldfeqlem1  37231  fprodcncf  37350  dvnmptdivc  37381  dvnxpaek  37385  dvnmul  37386  dvmptfprod  37388  dvnprodlem1  37389  dvnprodlem2  37390  dvnprodlem3  37391  dvnprod  37392  stoweidlem2  37430  stoweidlem17  37445  stoweidlem19  37447  stoweidlem20  37448  stoweidlem43  37472  stoweidlem62  37491  stoweidlem62OLD  37492  stoweid  37493  dirkercncflem2  37534  fourierdlem112  37649  fourierdlem113  37650  etransclem1  37666  etransclem5  37670  etransclem17  37682  etransclem19  37684  etransclem22  37687  sge0val  37741  c0rhm  38669  c0rnghm  38670  lincop  38960  aacllem  39300