Theorem mpteq2dv 5268

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

Hypothesis

Ref	Expression
mpteq2dv.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dv	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dv

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5266	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  ofeqd  7716  mpocurryvald  8311  rdgeq1  8467  rdgeq2  8468  omv  8568  oev  8570  oieq1  9581  oieq2  9582  cantnflem1  9758  wunex2  10807  wuncval2  10816  rpnnen1  13048  seqof2  14111  relexpsucnnr  15074  relexp1g  15075  limsupval  15520  sumeq2w  15740  sumeq2ii  15741  cbvsum  15743  cbvsumv  15744  sumeq2sdv  15751  summo  15765  fsum  15768  fsumrlim  15859  fsumo1  15860  prodeq1  15955  prodeq2w  15958  prodeq2sdv  15971  prodmo  15984  fprod  15989  bpolylem  16096  rpnnen2lem1  16262  rpnnen2lem2  16263  1arithlem1  16970  vdwapval  17020  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  vdwlem10  17037  ramub1lem2  17074  ramcl  17076  sloteq  17230  prdsplusgval  17533  prdsmulrval  17535  prdsdsval  17538  prdsvscaval  17539  ismon  17794  fucco  18032  curf1  18295  curf2  18299  yonedalem4a  18345  smndex1gbas  18937  smndex1gid  18938  grplactfval  19081  galactghm  19446  pmtrval  19493  sylow1  19645  sylow2b  19665  sylow3lem5  19673  sylow3  19675  iscyg  19921  gsumzaddlem  19963  gsumzmhm  19979  ablfac2  20133  gsumdixp  20342  c0rhm  20560  c0rnghm  20561  zncyg  21590  phllmhm  21673  isphld  21695  frlmgsum  21815  frlmipval  21822  frlmphl  21824  uvcval  21828  fczpsrbag  21964  psrmulfval  21986  psrascl  22022  mvrval  22025  subrgmvr  22074  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  mplmon2  22108  subrgascl  22113  evlslem2  22126  evlslem3  22127  evlslem1  22129  mpfrcl  22132  evlsval  22133  evlsvar  22137  mpfind  22154  selvfval  22161  selvval  22162  mhpfval  22165  psdfval  22185  psdval  22186  coe1fval  22228  pf1ind  22380  evl1gsumadd  22383  rhmmpl  22408  rhmply1vr1  22412  mamuval  22418  mamufv  22419  matgsum  22464  madetsumid  22488  mat1dimmul  22503  mvmulval  22570  mvmulfv  22571  mavmulfv  22573  1mavmul  22575  marepvval0  22593  mulmarep1gsum1  22600  mdetleib  22614  mdetleib2  22615  mdetfval1  22617  mdetleib1  22618  mdet0pr  22619  m1detdiag  22624  mdetralt  22635  mdetunilem9  22647  m2detleib  22658  smadiadetlem3  22695  mat2pmatmul  22758  decpmatmul  22799  decpmatmulsumfsupp  22800  pmatcollpw1  22803  monmatcollpw  22806  pmatcollpw3lem  22810  pmatcollpw3fi1lem2  22814  pm2mpval  22822  pm2mpfval  22823  mply1topmatval  22831  mp2pm2mplem1  22833  mp2pm2mplem3  22835  ptbasfi  23610  ptcnplem  23650  ptrescn  23668  cnmpt2k  23717  xkohmeo  23844  fmval  23972  fmf  23974  ptcmpg  24086  tmdmulg  24121  prdstmdd  24153  tsmspropd  24161  prdsxmslem2  24563  metdsval  24888  fsumcn  24913  expcn  24915  expcnOLD  24917  lebnumlem3  25014  pcoval  25063  pi1xfrcnv  25109  cphsscph  25304  rrxds  25446  rrxmval  25458  itg11  25745  mbfi1fseqlem2  25771  mbfi1fseqlem6  25775  mbfi1fseq  25776  mbfi1flimlem  25777  mbfmullem  25780  itg2const  25795  itg2mulc  25802  itg2monolem1  25805  itg2i1fseqle  25809  itg2i1fseq  25810  itg2addlem  25813  itg2cnlem1  25816  itg2cn  25818  isibl  25820  isibl2  25821  iblitg  25823  itgeq1  25828  itgz  25836  itgvallem  25840  itgvallem3  25841  iblcnlem1  25843  itgcnlem  25845  iblrelem  25846  iblposlem  25847  iblpos  25848  itgrevallem1  25850  itgposval  25851  iblss2  25861  itgss  25867  itgfsum  25882  iblabslem  25883  iblmulc2  25886  bddmulibl  25894  itgcn  25900  ellimc  25928  dvnfval  25978  cpnfval  25988  dvexp  26011  dvexp2  26012  dvmptfsum  26033  dvlipcn  26053  dvivthlem1  26067  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgpowd  26111  elply2  26255  elplyr  26260  elplyd  26261  coeeu  26284  coelem  26285  coeeq  26286  plyco  26300  coe11  26312  coe1termlem  26317  dgrcolem1  26333  dvply2g  26344  dvply2gOLD  26345  elqaalem3  26381  eltayl  26419  tayl0  26421  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmcau  26456  ulmdvlem1  26461  ulmdvlem3  26463  mtest  26465  mtestbdd  26466  pserval  26471  pserulm  26483  psercn  26488  pserdvlem2  26490  abelthlem3  26495  logtayl  26720  dvcxp1  26800  dvcncxp1  26803  logbmpt  26849  dmarea  27018  lgamgulmlem2  27091  lgamgulmlem5  27094  musum  27252  dchrptlem2  27327  dchrptlem3  27328  dchrpt  27329  lgsval  27363  lgsval4lem  27370  lgsneg  27383  lgsmod  27385  rpvmasum2  27574  padicfval  27678  ostth2  27699  ostth3  27700  ostth  27701  lmif  28811  islmib  28813  incistruhgr  29114  eucrct2eupth  30277  htthlem  30949  htth  30950  pjhfval  31428  hosmval  31767  hommval  31768  hodmval  31769  hfsmval  31770  hfmmval  31771  brafval  31975  kbfval  31984  mptprop  32710  psgnfzto1st  33098  linds2eq  33374  elrspunidl  33421  elrspunsn  33422  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  evls1fldgencl  33680  mdetpmtr1  33769  zar0ring  33824  ordtcnvNEW  33866  ordtrest2NEW  33869  xrhval  33964  indval  33977  esum2dlem  34056  ofceq  34061  itgeq12dv  34291  ballotlemfval  34454  vtsval  34614  lpadval  34653  ptpconn  35201  cvmliftlem15  35266  cvmlift2lem4  35274  cvmlift2  35284  snmlval  35299  snmlflim  35300  satf  35321  mrsubfval  35476  mrsubrn  35481  elmsubrn  35496  msubrn  35497  msubco  35499  faclim  35708  faclim2  35710  prodeq12sdv  36184  itgeq12sdv  36185  cbvsumdavw  36245  cbvproddavw  36246  cbvsumdavw2  36261  cbvproddavw2  36262  knoppcnlem1  36459  knoppcnlem6  36464  knoppcnlem7  36465  bj-evaleq  37038  csbrdgg  37295  curfv  37560  matunitlindflem2  37577  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem27  37607  voliunnfl  37624  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  iblabsnclem  37643  iblmulc2nc  37645  ftc1anclem2  37654  ftc1anclem6  37658  ftc1anclem8  37660  ftc1anc  37661  ftc2nc  37662  upixp  37689  rrncmslem  37792  ismrer1  37798  tendoplcbv  40732  tendopl  40733  tendoicbv  40750  tendoi  40751  dihfval  41188  lcfl7N  41458  lcfrlem8  41506  lcfrlem9  41507  lcf1o  41508  hvmapval  41717  hdmap1fval  41753  hdmapffval  41783  hdmapfval  41784  hgmapffval  41842  hgmapfval  41843  lcmineqlem7  41992  lcmineqlem12  41997  aks6d1c6lem5  42134  rhmpsr  42507  evlsvval  42515  evlsvvval  42518  evlsbagval  42521  selvvvval  42540  evlselv  42542  fsuppind  42545  fsuppssindlem2  42547  fsuppssind  42548  mzpclval  42681  mzpcl2  42686  mzpexpmpt  42701  mzpsubst  42704  mzpcompact2lem  42707  rmxfval  42860  rmyfval  42861  aomclem8  43018  hbtlem1  43080  hbtlem7  43082  rfovfvd  43964  fsovrfovd  43971  fsovfvd  43972  fsovcnvlem  43975  dssmapfv2d  43980  dssmapnvod  43982  ntrneibex  44035  mnringmulrvald  44196  mnringmulrcld  44197  expgrowthi  44302  expgrowth  44304  binomcxplemdvsum  44324  addrval  44435  subrval  44436  mulvval  44437  fmulcl  45502  fmuldfeqlem1  45503  fprodcnlem  45520  fprodcn  45521  fnlimfv  45584  fnlimcnv  45588  fnlimfvre  45595  fnlimfvre2  45598  fnlimf  45599  fnlimabslt  45600  liminfval  45680  limsupresxr  45687  liminfresxr  45688  liminfvalxr  45704  fprodcncf  45821  dvnmptdivc  45859  dvnxpaek  45863  dvnmul  45864  dvmptfprod  45866  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  dvnprod  45870  stoweidlem2  45923  stoweidlem17  45938  stoweidlem19  45940  stoweidlem20  45941  stoweidlem43  45964  stoweidlem62  45983  stoweid  45984  dirkercncflem2  46025  fourierdlem112  46139  fourierdlem113  46140  etransclem1  46156  etransclem5  46160  etransclem17  46172  etransclem19  46174  etransclem22  46177  sge0val  46287  ovnlecvr  46479  ovncvrrp  46485  ovn0lem  46486  ovnsubaddlem1  46491  ovnsubadd  46493  hsphoif  46497  hsphoival  46500  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hoidmvle  46521  ovnhoilem1  46522  ovnhoi  46524  hoidifhspval  46529  ovncvr2  46532  hoidifhspval2  46536  hspmbllem2  46548  hspmbllem3  46549  hspmbl  46550  ovnovollem1  46577  vonioolem2  46602  vonioo  46603  vonicclem2  46605  vonicc  46606  smflimlem4  46695  smflim  46698  smflim2  46727  smfsuplem2  46733  smfsup  46735  smfinf  46739  smflimsuplem2  46742  smflimsuplem5  46745  smflimsuplem7  46747  smflimsup  46749  cfsetsnfsetfo  46975  lincop  48137  1arymaptfv  48374  itcoval  48395  itcovalpc  48406  itcovalt2  48411  ackvalsuc1mpt  48412  ackval1  48415  aacllem  48895