Theorem mpteq2dv 4524

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 4523	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804   |-> cmpt 4495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-opab 4496  df-mpt 4497

This theorem is referenced by:  ofeq  6527  mpt2curryvald  7001  rdgeq1  7079  rdgeq2  7080  omv  7164  oev  7166  oieq1  7940  oieq2  7941  cantnffvalOLD  8085  cantnflem1  8111  cantnflem1OLD  8134  wunex2  9119  wuncval2  9128  reexALT  11224  seqof2  12146  limsupval  13278  sumeq2w  13495  sumeq2ii  13496  cbvsum  13498  summo  13520  fsum  13523  fsumrlim  13606  fsumo1  13607  prodeq2w  13700  prodmo  13724  fprod  13729  rpnnen2lem1  13929  rpnnen2lem2  13930  rpnnen  13941  1arithlem1  14422  vdwapval  14472  vdwlem6  14485  vdwlem8  14487  vdwlem9  14488  vdwlem10  14489  ramub1lem2  14526  ramcl  14528  prdsplusgval  14851  prdsmulrval  14853  prdsdsval  14856  prdsvscaval  14857  ismon  15109  fucco  15309  curf1  15472  curf2  15476  yonedalem4a  15522  grplactfval  16114  galactghm  16406  pmtrval  16454  sylow1  16601  sylow2b  16621  sylow3lem5  16629  sylow3  16631  iscyg  16860  gsumzaddlem  16912  gsumzaddlemOLD  16914  gsumzmhm  16935  gsumzmhmOLD  16936  ablfac2  17118  gsumdixpOLD  17235  gsumdixp  17236  fczpsrbag  17994  psrmulfval  18016  mvrval  18055  subrgmvr  18101  mplcoe1  18105  mplcoe3  18106  mplcoe3OLD  18107  mplcoe5  18109  mplcoe2OLD  18111  mplmon2  18136  subrgascl  18141  evlslem2  18158  evlslem3  18161  evlslem1  18162  mpfrcl  18165  evlsval  18166  evlsvar  18170  mpfind  18183  coe1fval  18222  pf1ind  18369  evl1gsumadd  18372  zncyg  18564  phllmhm  18644  isphld  18666  frlmgsumOLD  18778  frlmgsum  18779  frlmipval  18787  frlmphl  18789  uvcval  18793  mamuval  18865  mamufv  18866  matgsum  18916  madetsumid  18940  mat1dimmul  18955  mvmulval  19022  mvmulfv  19023  mavmulfv  19025  1mavmul  19027  marepvval0  19045  mulmarep1gsum1  19052  mdetleib  19066  mdetleib2  19067  mdetfval1  19069  mdetleib1  19070  mdet0pr  19071  m1detdiag  19076  mdetralt  19087  mdetunilem9  19099  m2detleib  19110  smadiadetlem3  19147  mat2pmatmul  19209  decpmatmul  19250  decpmatmulsumfsupp  19251  pmatcollpw1  19254  monmatcollpw  19257  pmatcollpw3lem  19261  pmatcollpw3fi1lem2  19265  pm2mpval  19273  pm2mpfval  19274  mply1topmatval  19282  mp2pm2mplem1  19284  mp2pm2mplem3  19286  ptbasfi  20059  ptcnplem  20099  ptrescn  20117  cnmpt2k  20166  xkohmeo  20293  fmval  20421  fmf  20423  ptcmpg  20534  tmdmulg  20568  prdstmdd  20599  tsmspropd  20607  prdsxmslem2  21009  metdsval  21328  fsumcn  21351  expcn  21353  lebnumlem3  21440  pcoval  21488  pi1xfrcnv  21534  rrxds  21802  rrxmval  21809  itg11  22075  mbfi1fseqlem2  22100  mbfi1fseqlem6  22104  mbfi1fseq  22105  mbfi1flimlem  22106  mbfmullem  22109  itg2const  22124  itg2mulc  22131  itg2monolem1  22134  itg2i1fseqle  22138  itg2i1fseq  22139  itg2addlem  22142  itg2cnlem1  22145  itg2cn  22147  isibl  22149  isibl2  22150  iblitg  22152  itgz  22164  itgvallem  22168  itgvallem3  22169  iblcnlem1  22171  itgcnlem  22173  iblrelem  22174  iblposlem  22175  iblpos  22176  itgrevallem1  22178  itgposval  22179  iblss2  22189  itgss  22195  itgfsum  22210  iblabslem  22211  iblmulc2  22214  bddmulibl  22222  itgcn  22226  ellimc  22254  dvnfval  22302  cpnfval  22312  dvexp  22333  dvexp2  22334  dvmptfsum  22353  dvlipcn  22372  dvivthlem1  22386  dvfsumle  22399  dvfsumabs  22401  dvfsumlem2  22405  elply2  22570  elplyr  22575  elplyd  22576  coeeu  22599  coelem  22600  coeeq  22601  plyco  22615  coe11  22626  coe1termlem  22631  dgrcolem1  22646  dvply2g  22657  elqaalem3  22693  eltayl  22731  tayl0  22733  taylthlem1  22744  taylthlem2  22745  ulmcau  22766  ulmdvlem1  22771  ulmdvlem3  22773  mtest  22775  mtestbdd  22776  pserval  22781  pserulm  22793  psercn  22797  pserdvlem2  22799  abelthlem3  22804  logtayl  23017  dvcxp1  23092  dmarea  23263  musum  23443  dchrptlem2  23516  dchrptlem3  23517  dchrpt  23518  lgsval  23551  lgsval4lem  23558  lgsneg  23570  lgsmod  23572  rpvmasum2  23673  padicfval  23777  ostth2  23798  ostth3  23799  ostth  23800  lmif  24127  islmib  24129  wwlkn  24658  clwwlkn  24743  clwwlknprop  24748  htthlem  25810  htth  25811  pjhfval  26290  hosmval  26630  hommval  26631  hodmval  26632  hfsmval  26633  hfmmval  26634  brafval  26838  kbfval  26847  ordtcnvNEW  27879  ordtrest2NEW  27882  xrhval  27973  indval  28004  ofceq  28073  itgeq12dv  28245  ballotlemfval  28405  lgamgulmlem2  28549  lgamgulmlem5  28552  ptpcon  28655  cvmliftlem15  28720  cvmlift2lem4  28728  cvmlift2  28738  snmlval  28753  snmlflim  28754  mrsubfval  28845  mrsubrn  28850  elmsubrn  28865  msubrn  28866  msubco  28868  relexp0  29029  relexpsucr  29030  faclim  29146  faclim2  29148  trpredeq1  29278  trpredeq2  29279  bpolylem  29785  voliunnfl  30033  itg2addnclem  30041  itg2addnclem3  30043  itg2addnc  30044  itg2gt0cn  30045  iblabsnclem  30053  iblmulc2nc  30055  ftc1anclem2  30066  ftc1anclem6  30070  ftc1anclem8  30072  ftc1anc  30073  ftc2nc  30074  dvcncxp1  30075  upixp  30195  rrncmslem  30303  ismrer1  30309  mzpclval  30632  mzpcl2  30637  mzpexpmpt  30652  mzpsubst  30656  mzpcompact2lem  30659  rmxfval  30815  rmyfval  30816  aomclem8  30982  hbtlem1  31047  hbtlem7  31049  itgpowd  31158  expgrowthi  31214  expgrowth  31216  addrval  31329  subrval  31330  mulvval  31331  fmulcl  31503  fmuldfeqlem1  31504  stoweidlem2  31673  stoweidlem17  31688  stoweidlem19  31690  stoweidlem20  31691  stoweidlem43  31714  stoweidlem62  31733  stoweid  31734  dirkercncflem2  31775  fourierdlem112  31890  fourierdlem113  31891  lincop  32744  tendoplcbv  36241  tendopl  36242  tendoicbv  36259  tendoi  36260  dihfval  36698  lcfl7N  36968  lcfrlem8  37016  lcfrlem9  37017  lcf1o  37018  hvmapval  37227  hdmap1fval  37264  hdmapffval  37296  hdmapfval  37297  hgmapffval  37355  hgmapfval  37356