Theorem mpteq2dv 4506

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

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898   |-> cmpt 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-ral 2754  df-opab 4478  df-mpt 4479

This theorem is referenced by:  ofeq  6565  mpt2curryvald  7048  rdgeq1  7160  rdgeq2  7161  omv  7245  oev  7247  oieq1  8058  oieq2  8059  cantnflem1  8225  wunex2  9194  wuncval2  9203  reexALT  11330  seqof2  12309  relexpsucnnr  13143  relexp1g  13144  limsupval  13586  limsupvalOLD  13587  sumeq2w  13813  sumeq2ii  13814  cbvsum  13816  summo  13838  fsum  13841  fsumrlim  13926  fsumo1  13927  prodeq2w  14021  prodmo  14045  fprod  14050  bpolylem  14156  rpnnen2lem1  14322  rpnnen2lem2  14323  rpnnen  14334  1arithlem1  14922  vdwapval  14978  vdwlem6  14991  vdwlem8  14993  vdwlem9  14994  vdwlem10  14995  ramub1lem2  15040  ramcl  15042  prdsplusgval  15426  prdsmulrval  15428  prdsdsval  15431  prdsvscaval  15432  ismon  15693  fucco  15922  curf1  16165  curf2  16169  yonedalem4a  16215  grplactfval  16807  galactghm  17099  pmtrval  17147  sylow1  17310  sylow2b  17330  sylow3lem5  17338  sylow3  17340  iscyg  17569  gsumzaddlem  17609  gsumzmhm  17625  ablfac2  17777  gsumdixp  17892  fczpsrbag  18646  psrmulfval  18664  mvrval  18700  subrgmvr  18740  mplcoe1  18744  mplcoe3  18745  mplcoe5  18747  mplmon2  18771  subrgascl  18776  evlslem2  18790  evlslem3  18792  evlslem1  18793  mpfrcl  18796  evlsval  18797  evlsvar  18801  mpfind  18814  coe1fval  18853  pf1ind  18998  evl1gsumadd  19001  zncyg  19174  phllmhm  19254  isphld  19276  frlmgsum  19385  frlmipval  19392  frlmphl  19394  uvcval  19398  mamuval  19466  mamufv  19467  matgsum  19517  madetsumid  19541  mat1dimmul  19556  mvmulval  19623  mvmulfv  19624  mavmulfv  19626  1mavmul  19628  marepvval0  19646  mulmarep1gsum1  19653  mdetleib  19667  mdetleib2  19668  mdetfval1  19670  mdetleib1  19671  mdet0pr  19672  m1detdiag  19677  mdetralt  19688  mdetunilem9  19700  m2detleib  19711  smadiadetlem3  19748  mat2pmatmul  19810  decpmatmul  19851  decpmatmulsumfsupp  19852  pmatcollpw1  19855  monmatcollpw  19858  pmatcollpw3lem  19862  pmatcollpw3fi1lem2  19866  pm2mpval  19874  pm2mpfval  19875  mply1topmatval  19883  mp2pm2mplem1  19885  mp2pm2mplem3  19887  ptbasfi  20651  ptcnplem  20691  ptrescn  20709  cnmpt2k  20758  xkohmeo  20885  fmval  21013  fmf  21015  ptcmpg  21127  tmdmulg  21162  prdstmdd  21193  tsmspropd  21201  prdsxmslem2  21599  metdsval  21919  metdsvalOLD  21934  fsumcn  21957  expcn  21959  lebnumlem3  22046  lebnumlem3OLD  22049  pcoval  22097  pi1xfrcnv  22143  rrxds  22407  rrxmval  22414  itg11  22705  mbfi1fseqlem2  22730  mbfi1fseqlem6  22734  mbfi1fseq  22735  mbfi1flimlem  22736  mbfmullem  22739  itg2const  22754  itg2mulc  22761  itg2monolem1  22764  itg2i1fseqle  22768  itg2i1fseq  22769  itg2addlem  22772  itg2cnlem1  22775  itg2cn  22777  isibl  22779  isibl2  22780  iblitg  22782  itgz  22794  itgvallem  22798  itgvallem3  22799  iblcnlem1  22801  itgcnlem  22803  iblrelem  22804  iblposlem  22805  iblpos  22806  itgrevallem1  22808  itgposval  22809  iblss2  22819  itgss  22825  itgfsum  22840  iblabslem  22841  iblmulc2  22844  bddmulibl  22852  itgcn  22856  ellimc  22884  dvnfval  22932  cpnfval  22942  dvexp  22963  dvexp2  22964  dvmptfsum  22983  dvlipcn  23002  dvivthlem1  23016  dvfsumle  23029  dvfsumabs  23031  dvfsumlem2  23035  elply2  23206  elplyr  23211  elplyd  23212  coeeu  23235  coelem  23236  coeeq  23237  plyco  23251  coe11  23263  coe1termlem  23268  dgrcolem1  23283  dvply2g  23294  elqaalem3  23330  elqaalem3OLD  23333  eltayl  23371  tayl0  23373  taylthlem1  23384  taylthlem2  23385  ulmcau  23406  ulmdvlem1  23411  ulmdvlem3  23413  mtest  23415  mtestbdd  23416  pserval  23421  pserulm  23433  psercn  23437  pserdvlem2  23439  abelthlem3  23444  logtayl  23661  dvcxp1  23736  dvcncxp1  23739  logbmpt  23781  dmarea  23939  lgamgulmlem2  24011  lgamgulmlem5  24014  musum  24176  dchrptlem2  24249  dchrptlem3  24250  dchrpt  24251  lgsval  24284  lgsval4lem  24291  lgsneg  24303  lgsmod  24305  rpvmasum2  24406  padicfval  24510  ostth2  24531  ostth3  24532  ostth  24533  lmif  24883  islmib  24885  wwlkn  25466  clwwlkn  25551  clwwlknprop  25556  htthlem  26626  htth  26627  pjhfval  27105  hosmval  27444  hommval  27445  hodmval  27446  hfsmval  27447  hfmmval  27448  brafval  27652  kbfval  27661  psgnfzto1st  28669  mdetpmtr1  28700  ordtcnvNEW  28777  ordtrest2NEW  28780  xrhval  28873  indval  28886  esum2dlem  28964  ofceq  28969  itgeq12dv  29209  ballotlemfval  29372  ptpcon  30006  cvmliftlem15  30071  cvmlift2lem4  30079  cvmlift2  30089  snmlval  30104  snmlflim  30105  mrsubfval  30196  mrsubrn  30201  elmsubrn  30216  msubrn  30217  msubco  30219  faclim  30432  faclim2  30434  trpredeq1  30511  trpredeq2  30512  csbrdgg  31776  poimirlem5  31991  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem10  31996  poimirlem11  31997  poimirlem12  31998  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem27  32013  voliunnfl  32030  itg2addnclem  32039  itg2addnclem3  32041  itg2addnc  32042  itg2gt0cn  32043  iblabsnclem  32051  iblmulc2nc  32053  ftc1anclem2  32064  ftc1anclem6  32068  ftc1anclem8  32070  ftc1anc  32071  ftc2nc  32072  upixp  32102  rrncmslem  32210  ismrer1  32216  tendoplcbv  34388  tendopl  34389  tendoicbv  34406  tendoi  34407  dihfval  34845  lcfl7N  35115  lcfrlem8  35163  lcfrlem9  35164  lcf1o  35165  hvmapval  35374  hdmap1fval  35411  hdmapffval  35443  hdmapfval  35444  hgmapffval  35502  hgmapfval  35503  mzpclval  35613  mzpcl2  35618  mzpexpmpt  35633  mzpsubst  35636  mzpcompact2lem  35639  rmxfval  35798  rmyfval  35799  aomclem8  35965  hbtlem1  36028  hbtlem7  36030  itgpowd  36145  expgrowthi  36727  expgrowth  36729  binomcxplemdvsum  36749  addrval  36864  subrval  36865  mulvval  36866  fmulcl  37745  fmuldfeqlem1  37746  fprodcncf  37865  dvnmptdivc  37899  dvnxpaek  37903  dvnmul  37904  dvmptfprod  37906  dvnprodlem1  37907  dvnprodlem2  37908  dvnprodlem3  37909  dvnprod  37910  stoweidlem2  37963  stoweidlem17  37978  stoweidlem19  37980  stoweidlem20  37981  stoweidlem43  38005  stoweidlem62  38024  stoweidlem62OLD  38025  stoweid  38026  dirkercncflem2  38067  fourierdlem112  38183  fourierdlem113  38184  etransclem1  38201  etransclem5  38205  etransclem17  38217  etransclem19  38219  etransclem22  38222  sge0val  38311  ovnlecvr  38487  ovncvrrp  38493  ovn0lem  38494  ovnsubaddlem1  38499  ovnsubadd  38501  hsphoif  38505  hsphoival  38508  hoidmv1lelem1  38520  hoidmv1lelem2  38521  hoidmv1lelem3  38522  hoidmv1le  38523  hoidmvlelem1  38524  hoidmvlelem2  38525  hoidmvlelem3  38526  hoidmvlelem4  38527  hoidmvlelem5  38528  hoidmvle  38529  ovnhoilem1  38530  ovnhoi  38532  hoidifhspval  38537  ovncvr2  38540  hoidifhspval2  38544  hspmbllem2  38556  hspmbllem3  38557  hspmbl  38558  ovnovollem1  38585  incistruhgr  39314  c0rhm  40281  c0rnghm  40282  lincop  40570  aacllem  40909