Theorem mpteq2dv 5177

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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5175	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ↦ cmpt 5158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-opab 5138  df-mpt 5159

This theorem is referenced by:  ofeqd  7544  mpocurryvald  8095  rdgeq1  8251  rdgeq2  8252  omv  8351  oev  8353  oieq1  9280  oieq2  9281  cantnflem1  9456  wunex2  10503  wuncval2  10512  rpnnen1  12732  seqof2  13790  relexpsucnnr  14745  relexp1g  14746  limsupval  15192  sumeq2w  15413  sumeq2ii  15414  cbvsum  15416  summo  15438  fsum  15441  fsumrlim  15532  fsumo1  15533  prodeq2w  15631  prodmo  15655  fprod  15660  bpolylem  15767  rpnnen2lem1  15932  rpnnen2lem2  15933  1arithlem1  16633  vdwapval  16683  vdwlem6  16696  vdwlem8  16698  vdwlem9  16699  vdwlem10  16700  ramub1lem2  16737  ramcl  16739  sloteq  16893  prdsplusgval  17193  prdsmulrval  17195  prdsdsval  17198  prdsvscaval  17199  ismon  17454  fucco  17689  curf1  17952  curf2  17956  yonedalem4a  18002  smndex1gbas  18550  smndex1gid  18551  grplactfval  18685  galactghm  19021  pmtrval  19068  sylow1  19217  sylow2b  19237  sylow3lem5  19245  sylow3  19247  iscyg  19488  gsumzaddlem  19531  gsumzmhm  19547  ablfac2  19701  gsumdixp  19857  zncyg  20765  phllmhm  20846  isphld  20868  frlmgsum  20988  frlmipval  20995  frlmphl  20997  uvcval  21001  fczpsrbag  21135  psrmulfval  21163  mvrval  21199  subrgmvr  21243  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  mplmon2  21278  subrgascl  21283  evlslem2  21298  evlslem3  21299  evlslem1  21301  mpfrcl  21304  evlsval  21305  evlsvar  21309  mpfind  21326  selvfval  21336  selvval  21337  mhpfval  21338  coe1fval  21385  pf1ind  21530  evl1gsumadd  21533  mamuval  21544  mamufv  21545  matgsum  21595  madetsumid  21619  mat1dimmul  21634  mvmulval  21701  mvmulfv  21702  mavmulfv  21704  1mavmul  21706  marepvval0  21724  mulmarep1gsum1  21731  mdetleib  21745  mdetleib2  21746  mdetfval1  21748  mdetleib1  21749  mdet0pr  21750  m1detdiag  21755  mdetralt  21766  mdetunilem9  21778  m2detleib  21789  smadiadetlem3  21826  mat2pmatmul  21889  decpmatmul  21930  decpmatmulsumfsupp  21931  pmatcollpw1  21934  monmatcollpw  21937  pmatcollpw3lem  21941  pmatcollpw3fi1lem2  21945  pm2mpval  21953  pm2mpfval  21954  mply1topmatval  21962  mp2pm2mplem1  21964  mp2pm2mplem3  21966  ptbasfi  22741  ptcnplem  22781  ptrescn  22799  cnmpt2k  22848  xkohmeo  22975  fmval  23103  fmf  23105  ptcmpg  23217  tmdmulg  23252  prdstmdd  23284  tsmspropd  23292  prdsxmslem2  23694  metdsval  24019  fsumcn  24042  expcn  24044  lebnumlem3  24135  pcoval  24183  pi1xfrcnv  24229  cphsscph  24424  rrxds  24566  rrxmval  24578  itg11  24864  mbfi1fseqlem2  24890  mbfi1fseqlem6  24894  mbfi1fseq  24895  mbfi1flimlem  24896  mbfmullem  24899  itg2const  24914  itg2mulc  24921  itg2monolem1  24924  itg2i1fseqle  24928  itg2i1fseq  24929  itg2addlem  24932  itg2cnlem1  24935  itg2cn  24937  isibl  24939  isibl2  24940  iblitg  24942  itgz  24954  itgvallem  24958  itgvallem3  24959  iblcnlem1  24961  itgcnlem  24963  iblrelem  24964  iblposlem  24965  iblpos  24966  itgrevallem1  24968  itgposval  24969  iblss2  24979  itgss  24985  itgfsum  25000  iblabslem  25001  iblmulc2  25004  bddmulibl  25012  itgcn  25018  ellimc  25046  dvnfval  25095  cpnfval  25105  dvexp  25126  dvexp2  25127  dvmptfsum  25148  dvlipcn  25167  dvivthlem1  25181  dvfsumle  25194  dvfsumabs  25196  dvfsumlem2  25200  itgpowd  25223  elply2  25366  elplyr  25371  elplyd  25372  coeeu  25395  coelem  25396  coeeq  25397  plyco  25411  coe11  25423  coe1termlem  25428  dgrcolem1  25443  dvply2g  25454  elqaalem3  25490  eltayl  25528  tayl0  25530  taylthlem1  25541  taylthlem2  25542  ulmcau  25563  ulmdvlem1  25568  ulmdvlem3  25570  mtest  25572  mtestbdd  25573  pserval  25578  pserulm  25590  psercn  25594  pserdvlem2  25596  abelthlem3  25601  logtayl  25824  dvcxp1  25902  dvcncxp1  25905  logbmpt  25947  dmarea  26116  lgamgulmlem2  26188  lgamgulmlem5  26191  musum  26349  dchrptlem2  26422  dchrptlem3  26423  dchrpt  26424  lgsval  26458  lgsval4lem  26465  lgsneg  26478  lgsmod  26480  rpvmasum2  26669  padicfval  26773  ostth2  26794  ostth3  26795  ostth  26796  lmif  27155  islmib  27157  incistruhgr  27458  eucrct2eupth  28618  htthlem  29288  htth  29289  pjhfval  29767  hosmval  30106  hommval  30107  hodmval  30108  hfsmval  30109  hfmmval  30110  brafval  30314  kbfval  30323  mptprop  31040  psgnfzto1st  31381  linds2eq  31584  elrspunidl  31615  lbsdiflsp0  31716  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  mdetpmtr1  31782  zar0ring  31837  ordtcnvNEW  31879  ordtrest2NEW  31882  xrhval  31977  indval  31990  esum2dlem  32069  ofceq  32074  itgeq12dv  32302  ballotlemfval  32465  vtsval  32626  lpadval  32665  ptpconn  33204  cvmliftlem15  33269  cvmlift2lem4  33277  cvmlift2  33287  snmlval  33302  snmlflim  33303  satf  33324  mrsubfval  33479  mrsubrn  33484  elmsubrn  33499  msubrn  33500  msubco  33502  faclim  33721  faclim2  33723  knoppcnlem1  34682  knoppcnlem6  34687  knoppcnlem7  34688  bj-evaleq  35252  csbrdgg  35509  curfv  35766  matunitlindflem2  35783  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem27  35813  voliunnfl  35830  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  itg2gt0cn  35841  iblabsnclem  35849  iblmulc2nc  35851  ftc1anclem2  35860  ftc1anclem6  35864  ftc1anclem8  35866  ftc1anc  35867  ftc2nc  35868  upixp  35896  rrncmslem  35999  ismrer1  36005  tendoplcbv  38796  tendopl  38797  tendoicbv  38814  tendoi  38815  dihfval  39252  lcfl7N  39522  lcfrlem8  39570  lcfrlem9  39571  lcf1o  39572  hvmapval  39781  hdmap1fval  39817  hdmapffval  39847  hdmapfval  39848  hgmapffval  39906  hgmapfval  39907  lcmineqlem7  40050  lcmineqlem12  40055  evlsbagval  40282  fsuppind  40286  fsuppssindlem2  40288  fsuppssind  40289  mzpclval  40554  mzpcl2  40559  mzpexpmpt  40574  mzpsubst  40577  mzpcompact2lem  40580  rmxfval  40733  rmyfval  40734  aomclem8  40893  hbtlem1  40955  hbtlem7  40957  rfovfvd  41617  fsovrfovd  41624  fsovfvd  41625  fsovcnvlem  41628  dssmapfv2d  41633  dssmapnvod  41635  ntrneibex  41690  mnringmulrvald  41852  mnringmulrcld  41853  expgrowthi  41958  expgrowth  41960  binomcxplemdvsum  41980  addrval  42091  subrval  42092  mulvval  42093  fmulcl  43129  fmuldfeqlem1  43130  fprodcnlem  43147  fprodcn  43148  fnlimfv  43211  fnlimcnv  43215  fnlimfvre  43222  fnlimfvre2  43225  fnlimf  43226  fnlimabslt  43227  liminfval  43307  limsupresxr  43314  liminfresxr  43315  liminfvalxr  43331  fprodcncf  43448  dvnmptdivc  43486  dvnxpaek  43490  dvnmul  43491  dvmptfprod  43493  dvnprodlem1  43494  dvnprodlem2  43495  dvnprodlem3  43496  dvnprod  43497  stoweidlem2  43550  stoweidlem17  43565  stoweidlem19  43567  stoweidlem20  43568  stoweidlem43  43591  stoweidlem62  43610  stoweid  43611  dirkercncflem2  43652  fourierdlem112  43766  fourierdlem113  43767  etransclem1  43783  etransclem5  43787  etransclem17  43799  etransclem19  43801  etransclem22  43804  sge0val  43911  ovnlecvr  44103  ovncvrrp  44109  ovn0lem  44110  ovnsubaddlem1  44115  ovnsubadd  44117  hsphoif  44121  hsphoival  44124  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvlelem5  44144  hoidmvle  44145  ovnhoilem1  44146  ovnhoi  44148  hoidifhspval  44153  ovncvr2  44156  hoidifhspval2  44160  hspmbllem2  44172  hspmbllem3  44173  hspmbl  44174  ovnovollem1  44201  vonioolem2  44226  vonioo  44227  vonicclem2  44229  vonicc  44230  smflimlem4  44319  smflim  44322  smflim2  44350  smfsuplem2  44356  smfsup  44358  smfinf  44362  smflimsuplem2  44365  smflimsuplem5  44368  smflimsuplem7  44370  smflimsup  44372  cfsetsnfsetfo  44565  c0rhm  45481  c0rnghm  45482  lincop  45760  1arymaptfv  45997  itcoval  46018  itcovalpc  46029  itcovalt2  46034  ackvalsuc1mpt  46035  ackval1  46038  aacllem  46516