Theorem mpteq2dv 5189

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 5188	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-mpt 5177

This theorem is referenced by:  ifmpt2v  7457  ofeqd  7621  mpocurryvald  8209  rdgeq1  8339  rdgeq2  8340  omv  8436  oev  8438  oieq1  9409  oieq2  9410  cantnflem1  9590  wunex2  10640  wuncval2  10649  rpnnen1  12887  seqof2  13974  relexpsucnnr  14939  relexp1g  14940  limsupval  15388  sumeq2w  15606  sumeq2ii  15607  cbvsum  15609  cbvsumv  15610  sumeq2sdv  15617  summo  15631  fsum  15634  fsumrlim  15725  fsumo1  15726  prodeq1  15821  prodeq2w  15824  prodeq2sdv  15837  prodmo  15850  fprod  15855  bpolylem  15962  rpnnen2lem1  16130  rpnnen2lem2  16131  1arithlem1  16842  vdwapval  16892  vdwlem6  16905  vdwlem8  16907  vdwlem9  16908  vdwlem10  16909  ramub1lem2  16946  ramcl  16948  sloteq  17101  prdsplusgval  17384  prdsmulrval  17386  prdsdsval  17389  prdsvscaval  17390  ismon  17648  fucco  17880  curf1  18139  curf2  18143  yonedalem4a  18189  smndex1gbas  18818  smndex1gid  18819  grplactfval  18962  galactghm  19324  pmtrval  19371  sylow1  19523  sylow2b  19543  sylow3lem5  19551  sylow3  19553  iscyg  19799  gsumzaddlem  19841  gsumzmhm  19857  ablfac2  20011  gsumdixp  20245  c0rhm  20458  c0rnghm  20459  zncyg  21494  phllmhm  21578  isphld  21600  frlmgsum  21718  frlmipval  21725  frlmphl  21727  uvcval  21731  fczpsrbag  21868  psrmulfval  21890  psrascl  21925  mvrval  21928  subrgmvr  21979  mplcoe1  21983  mplcoe3  21984  mplcoe5  21986  mplmon2  22007  subrgascl  22012  evlslem2  22025  evlslem3  22026  evlslem1  22028  mpfrcl  22031  evlsval  22032  evlsvval  22036  evlsvvval  22039  evlsvar  22041  mpfind  22061  selvfval  22068  selvval  22069  mhpfval  22072  psdfval  22092  psdval  22093  psdmvr  22103  coe1fval  22137  pf1ind  22290  evl1gsumadd  22293  rhmmpl  22318  rhmply1vr1  22322  mamuval  22328  mamufv  22329  matgsum  22372  madetsumid  22396  mat1dimmul  22411  mvmulval  22478  mvmulfv  22479  mavmulfv  22481  1mavmul  22483  marepvval0  22501  mulmarep1gsum1  22508  mdetleib  22522  mdetleib2  22523  mdetfval1  22525  mdetleib1  22526  mdet0pr  22527  m1detdiag  22532  mdetralt  22543  mdetunilem9  22555  m2detleib  22566  smadiadetlem3  22603  mat2pmatmul  22666  decpmatmul  22707  decpmatmulsumfsupp  22708  pmatcollpw1  22711  monmatcollpw  22714  pmatcollpw3lem  22718  pmatcollpw3fi1lem2  22722  pm2mpval  22730  pm2mpfval  22731  mply1topmatval  22739  mp2pm2mplem1  22741  mp2pm2mplem3  22743  ptbasfi  23516  ptcnplem  23556  ptrescn  23574  cnmpt2k  23623  xkohmeo  23750  fmval  23878  fmf  23880  ptcmpg  23992  tmdmulg  24027  prdstmdd  24059  tsmspropd  24067  prdsxmslem2  24464  metdsval  24783  fsumcn  24808  expcn  24810  expcnOLD  24812  lebnumlem3  24909  pcoval  24958  pi1xfrcnv  25004  cphsscph  25198  rrxds  25340  rrxmval  25352  itg11  25639  mbfi1fseqlem2  25664  mbfi1fseqlem6  25668  mbfi1fseq  25669  mbfi1flimlem  25670  mbfmullem  25673  itg2const  25688  itg2mulc  25695  itg2monolem1  25698  itg2i1fseqle  25702  itg2i1fseq  25703  itg2addlem  25706  itg2cnlem1  25709  itg2cn  25711  isibl  25713  isibl2  25714  iblitg  25716  itgeq1  25721  itgz  25729  itgvallem  25733  itgvallem3  25734  iblcnlem1  25736  itgcnlem  25738  iblrelem  25739  iblposlem  25740  iblpos  25741  itgrevallem1  25743  itgposval  25744  iblss2  25754  itgss  25760  itgfsum  25775  iblabslem  25776  iblmulc2  25779  bddmulibl  25787  itgcn  25793  ellimc  25821  dvnfval  25871  cpnfval  25881  dvexp  25904  dvexp2  25905  dvmptfsum  25926  dvlipcn  25946  dvivthlem1  25960  dvfsumle  25973  dvfsumleOLD  25974  dvfsumabs  25976  dvfsumlem2  25980  dvfsumlem2OLD  25981  itgpowd  26004  elply2  26148  elplyr  26153  elplyd  26154  coeeu  26177  coelem  26178  coeeq  26179  plyco  26193  coe11  26205  coe1termlem  26210  dgrcolem1  26226  dvply2g  26239  dvply2gOLD  26240  elqaalem3  26276  eltayl  26314  tayl0  26316  taylthlem1  26328  taylthlem2  26329  taylthlem2OLD  26330  ulmcau  26351  ulmdvlem1  26356  ulmdvlem3  26358  mtest  26360  mtestbdd  26361  pserval  26366  pserulm  26378  psercn  26383  pserdvlem2  26385  abelthlem3  26390  logtayl  26616  dvcxp1  26696  dvcncxp1  26699  logbmpt  26745  dmarea  26914  lgamgulmlem2  26987  lgamgulmlem5  26990  musum  27148  dchrptlem2  27223  dchrptlem3  27224  dchrpt  27225  lgsval  27259  lgsval4lem  27266  lgsneg  27279  lgsmod  27281  rpvmasum2  27470  padicfval  27574  ostth2  27595  ostth3  27596  ostth  27597  lmif  28783  islmib  28785  incistruhgr  29078  eucrct2eupth  30246  htthlem  30918  htth  30919  pjhfval  31397  hosmval  31736  hommval  31737  hodmval  31738  hfsmval  31739  hfmmval  31740  brafval  31944  kbfval  31953  mptprop  32703  indval  32860  indsn  32873  psgnfzto1st  33115  fxpsubm  33182  fxpsubg  33183  fxpsubrg  33184  elrgspnlem1  33252  elrgspnlem2  33253  elrgspnlem3  33254  elrgspnlem4  33255  elrgspn  33256  elrgspnsubrunlem1  33257  linds2eq  33390  elrspunidl  33437  elrspunsn  33438  evl1deg1  33585  evl1deg2  33586  evl1deg3  33587  extvfval  33625  extvfv  33626  mvrvalind  33631  evlextv  33635  mplvrpmfgalem  33637  mplvrpmga  33638  mplvrpmmhm  33639  mplvrpmrhm  33640  splysubrg  33646  issply  33647  esplyval  33648  vietalem  33663  vieta  33664  lbsdiflsp0  33711  fedgmullem1  33714  fedgmullem2  33715  fedgmul  33716  evls1fldgencl  33755  fldextrspunlsplem  33758  fldextrspunlsp  33759  extdgfialglem2  33778  mdetpmtr1  33908  zar0ring  33963  ordtcnvNEW  34005  ordtrest2NEW  34008  xrhval  34103  esum2dlem  34177  ofceq  34182  itgeq12dv  34411  ballotlemfval  34575  vtsval  34722  lpadval  34761  ptpconn  35349  cvmliftlem15  35414  cvmlift2lem4  35422  cvmlift2  35432  snmlval  35447  snmlflim  35448  satf  35469  mrsubfval  35624  mrsubrn  35629  elmsubrn  35644  msubrn  35645  msubco  35647  faclim  35862  faclim2  35864  prodeq12sdv  36334  itgeq12sdv  36335  cbvsumdavw  36395  cbvproddavw  36396  cbvsumdavw2  36411  cbvproddavw2  36412  knoppcnlem1  36609  knoppcnlem6  36614  knoppcnlem7  36615  bj-evaleq  37189  csbrdgg  37446  curfv  37713  matunitlindflem2  37730  poimirlem5  37738  poimirlem6  37739  poimirlem7  37740  poimirlem8  37741  poimirlem10  37743  poimirlem11  37744  poimirlem12  37745  poimirlem15  37748  poimirlem16  37749  poimirlem17  37750  poimirlem18  37751  poimirlem19  37752  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem27  37760  voliunnfl  37777  itg2addnclem  37784  itg2addnclem3  37786  itg2addnc  37787  itg2gt0cn  37788  iblabsnclem  37796  iblmulc2nc  37798  ftc1anclem2  37807  ftc1anclem6  37811  ftc1anclem8  37813  ftc1anc  37814  ftc2nc  37815  upixp  37842  rrncmslem  37945  ismrer1  37951  tendoplcbv  40947  tendopl  40948  tendoicbv  40965  tendoi  40966  dihfval  41403  lcfl7N  41673  lcfrlem8  41721  lcfrlem9  41722  lcf1o  41723  hvmapval  41932  hdmap1fval  41968  hdmapffval  41998  hdmapfval  41999  hgmapffval  42057  hgmapfval  42058  lcmineqlem7  42201  lcmineqlem12  42206  aks6d1c6lem5  42343  rhmpsr  42720  evlsbagval  42727  selvvvval  42743  evlselv  42745  fsuppind  42748  fsuppssindlem2  42750  fsuppssind  42751  mzpclval  42882  mzpcl2  42887  mzpexpmpt  42902  mzpsubst  42905  mzpcompact2lem  42908  rmxfval  43061  rmyfval  43062  aomclem8  43218  hbtlem1  43280  hbtlem7  43282  rfovfvd  44159  fsovrfovd  44166  fsovfvd  44167  fsovcnvlem  44170  dssmapfv2d  44175  dssmapnvod  44177  ntrneibex  44230  mnringmulrvald  44384  mnringmulrcld  44385  expgrowthi  44490  expgrowth  44492  binomcxplemdvsum  44512  addrval  44622  subrval  44623  mulvval  44624  fmulcl  45743  fmuldfeqlem1  45744  fprodcnlem  45761  fprodcn  45762  fnlimfv  45823  fnlimcnv  45827  fnlimfvre  45834  fnlimfvre2  45837  fnlimf  45838  fnlimabslt  45839  liminfval  45919  limsupresxr  45926  liminfresxr  45927  liminfvalxr  45943  fprodcncf  46060  dvnmptdivc  46098  dvnxpaek  46102  dvnmul  46103  dvmptfprod  46105  dvnprodlem1  46106  dvnprodlem2  46107  dvnprodlem3  46108  dvnprod  46109  stoweidlem2  46162  stoweidlem17  46177  stoweidlem19  46179  stoweidlem20  46180  stoweidlem43  46203  stoweidlem62  46222  stoweid  46223  dirkercncflem2  46264  fourierdlem112  46378  fourierdlem113  46379  etransclem1  46395  etransclem5  46399  etransclem17  46411  etransclem19  46413  etransclem22  46416  sge0val  46526  ovnlecvr  46718  ovncvrrp  46724  ovn0lem  46725  ovnsubaddlem1  46730  ovnsubadd  46732  hsphoif  46736  hsphoival  46739  hoidmv1lelem1  46751  hoidmv1lelem2  46752  hoidmv1lelem3  46753  hoidmv1le  46754  hoidmvlelem1  46755  hoidmvlelem2  46756  hoidmvlelem3  46757  hoidmvlelem4  46758  hoidmvlelem5  46759  hoidmvle  46760  ovnhoilem1  46761  ovnhoi  46763  hoidifhspval  46768  ovncvr2  46771  hoidifhspval2  46775  hspmbllem2  46787  hspmbllem3  46788  hspmbl  46789  ovnovollem1  46816  vonioolem2  46841  vonioo  46842  vonicclem2  46844  vonicc  46845  smflimlem4  46934  smflim  46937  smflim2  46966  smfsuplem2  46972  smfsup  46974  smfinf  46978  smflimsuplem2  46981  smflimsuplem5  46984  smflimsuplem7  46986  smflimsup  46988  cfsetsnfsetfo  47222  lincop  48570  1arymaptfv  48802  itcoval  48823  itcovalpc  48834  itcovalt2  48839  ackvalsuc1mpt  48840  ackval1  48843  fuco21  49497  prcofval  49539  aacllem  49962