Theorem mpteq2dv 4526

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 1823   |-> cmpt 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-opab 4498  df-mpt 4499

This theorem is referenced by:  ofeq  6515  mpt2curryvald  6991  rdgeq1  7069  rdgeq2  7070  omv  7154  oev  7156  oieq1  7929  oieq2  7930  cantnffvalOLD  8073  cantnflem1  8099  cantnflem1OLD  8122  wunex2  9105  wuncval2  9114  reexALT  11215  seqof2  12150  relexpsucnnr  12945  relexp1g  12946  limsupval  13382  sumeq2w  13599  sumeq2ii  13600  cbvsum  13602  summo  13624  fsum  13627  fsumrlim  13710  fsumo1  13711  prodeq2w  13804  prodmo  13828  fprod  13833  rpnnen2lem1  14035  rpnnen2lem2  14036  rpnnen  14047  1arithlem1  14528  vdwapval  14578  vdwlem6  14591  vdwlem8  14593  vdwlem9  14594  vdwlem10  14595  ramub1lem2  14632  ramcl  14634  prdsplusgval  14965  prdsmulrval  14967  prdsdsval  14970  prdsvscaval  14971  ismon  15224  fucco  15453  curf1  15696  curf2  15700  yonedalem4a  15746  grplactfval  16338  galactghm  16630  pmtrval  16678  sylow1  16825  sylow2b  16845  sylow3lem5  16853  sylow3  16855  iscyg  17084  gsumzaddlem  17136  gsumzaddlemOLD  17138  gsumzmhm  17158  gsumzmhmOLD  17159  ablfac2  17338  gsumdixpOLD  17455  gsumdixp  17456  fczpsrbag  18214  psrmulfval  18236  mvrval  18275  subrgmvr  18321  mplcoe1  18325  mplcoe3  18326  mplcoe3OLD  18327  mplcoe5  18329  mplcoe2OLD  18331  mplmon2  18356  subrgascl  18361  evlslem2  18378  evlslem3  18381  evlslem1  18382  mpfrcl  18385  evlsval  18386  evlsvar  18390  mpfind  18403  coe1fval  18442  pf1ind  18589  evl1gsumadd  18592  zncyg  18763  phllmhm  18843  isphld  18865  frlmgsumOLD  18975  frlmgsum  18976  frlmipval  18984  frlmphl  18986  uvcval  18990  mamuval  19058  mamufv  19059  matgsum  19109  madetsumid  19133  mat1dimmul  19148  mvmulval  19215  mvmulfv  19216  mavmulfv  19218  1mavmul  19220  marepvval0  19238  mulmarep1gsum1  19245  mdetleib  19259  mdetleib2  19260  mdetfval1  19262  mdetleib1  19263  mdet0pr  19264  m1detdiag  19269  mdetralt  19280  mdetunilem9  19292  m2detleib  19303  smadiadetlem3  19340  mat2pmatmul  19402  decpmatmul  19443  decpmatmulsumfsupp  19444  pmatcollpw1  19447  monmatcollpw  19450  pmatcollpw3lem  19454  pmatcollpw3fi1lem2  19458  pm2mpval  19466  pm2mpfval  19467  mply1topmatval  19475  mp2pm2mplem1  19477  mp2pm2mplem3  19479  ptbasfi  20251  ptcnplem  20291  ptrescn  20309  cnmpt2k  20358  xkohmeo  20485  fmval  20613  fmf  20615  ptcmpg  20726  tmdmulg  20760  prdstmdd  20791  tsmspropd  20799  prdsxmslem2  21201  metdsval  21520  fsumcn  21543  expcn  21545  lebnumlem3  21632  pcoval  21680  pi1xfrcnv  21726  rrxds  21994  rrxmval  22001  itg11  22267  mbfi1fseqlem2  22292  mbfi1fseqlem6  22296  mbfi1fseq  22297  mbfi1flimlem  22298  mbfmullem  22301  itg2const  22316  itg2mulc  22323  itg2monolem1  22326  itg2i1fseqle  22330  itg2i1fseq  22331  itg2addlem  22334  itg2cnlem1  22337  itg2cn  22339  isibl  22341  isibl2  22342  iblitg  22344  itgz  22356  itgvallem  22360  itgvallem3  22361  iblcnlem1  22363  itgcnlem  22365  iblrelem  22366  iblposlem  22367  iblpos  22368  itgrevallem1  22370  itgposval  22371  iblss2  22381  itgss  22387  itgfsum  22402  iblabslem  22403  iblmulc2  22406  bddmulibl  22414  itgcn  22418  ellimc  22446  dvnfval  22494  cpnfval  22504  dvexp  22525  dvexp2  22526  dvmptfsum  22545  dvlipcn  22564  dvivthlem1  22578  dvfsumle  22591  dvfsumabs  22593  dvfsumlem2  22597  elply2  22762  elplyr  22767  elplyd  22768  coeeu  22791  coelem  22792  coeeq  22793  plyco  22807  coe11  22819  coe1termlem  22824  dgrcolem1  22839  dvply2g  22850  elqaalem3  22886  eltayl  22924  tayl0  22926  taylthlem1  22937  taylthlem2  22938  ulmcau  22959  ulmdvlem1  22964  ulmdvlem3  22966  mtest  22968  mtestbdd  22969  pserval  22974  pserulm  22986  psercn  22990  pserdvlem2  22992  abelthlem3  22997  logtayl  23212  dvcxp1  23287  logbmpt  23330  dmarea  23488  musum  23668  dchrptlem2  23741  dchrptlem3  23742  dchrpt  23743  lgsval  23776  lgsval4lem  23783  lgsneg  23795  lgsmod  23797  rpvmasum2  23898  padicfval  24002  ostth2  24023  ostth3  24024  ostth  24025  lmif  24355  islmib  24357  wwlkn  24887  clwwlkn  24972  clwwlknprop  24977  htthlem  26035  htth  26036  pjhfval  26515  hosmval  26855  hommval  26856  hodmval  26857  hfsmval  26858  hfmmval  26859  brafval  27063  kbfval  27072  ordtcnvNEW  28140  ordtrest2NEW  28143  xrhval  28233  indval  28246  esum2dlem  28324  ofceq  28329  itgeq12dv  28535  ballotlemfval  28695  lgamgulmlem2  28839  lgamgulmlem5  28842  ptpcon  28945  cvmliftlem15  29010  cvmlift2lem4  29018  cvmlift2  29028  snmlval  29043  snmlflim  29044  mrsubfval  29135  mrsubrn  29140  elmsubrn  29155  msubrn  29156  msubco  29158  faclim  29415  faclim2  29417  trpredeq1  29546  trpredeq2  29547  bpolylem  30041  voliunnfl  30301  itg2addnclem  30309  itg2addnclem3  30311  itg2addnc  30312  itg2gt0cn  30313  iblabsnclem  30321  iblmulc2nc  30323  ftc1anclem2  30334  ftc1anclem6  30338  ftc1anclem8  30340  ftc1anc  30341  ftc2nc  30342  dvcncxp1  30343  upixp  30463  rrncmslem  30571  ismrer1  30577  mzpclval  30900  mzpcl2  30905  mzpexpmpt  30920  mzpsubst  30923  mzpcompact2lem  30926  rmxfval  31082  rmyfval  31083  aomclem8  31249  hbtlem1  31316  hbtlem7  31318  itgpowd  31426  expgrowthi  31482  expgrowth  31484  binomcxplemdvsum  31504  addrval  31619  subrval  31620  mulvval  31621  fmulcl  31817  fmuldfeqlem1  31818  fprodcncf  31946  dvnmptdivc  31977  dvnxpaek  31981  dvnmul  31982  dvmptfprod  31984  dvnprodlem1  31985  dvnprodlem2  31986  dvnprodlem3  31987  dvnprod  31988  stoweidlem2  32026  stoweidlem17  32041  stoweidlem19  32043  stoweidlem20  32044  stoweidlem43  32067  stoweidlem62  32086  stoweid  32087  dirkercncflem2  32128  fourierdlem112  32243  fourierdlem113  32244  etransclem1  32260  etransclem5  32264  etransclem17  32276  etransclem19  32278  etransclem22  32281  c0rhm  32991  c0rnghm  32992  lincop  33282  aacllem  33623  tendoplcbv  36917  tendopl  36918  tendoicbv  36935  tendoi  36936  dihfval  37374  lcfl7N  37644  lcfrlem8  37692  lcfrlem9  37693  lcf1o  37694  hvmapval  37903  hdmap1fval  37940  hdmapffval  37972  hdmapfval  37973  hgmapffval  38031  hgmapfval  38032