Theorem mpteq2i 5181

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpteq2i.1	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
mpteq2i	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Proof of Theorem mpteq2i

Step	Hyp	Ref	Expression
1		mpteq2i.1	. . 3 ⊢ 𝐵 = 𝐶
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
3	2	mpteq2ia 5180	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  offval22  8038  offsplitfpar  8069  konigth  10492  ofccat  14931  rlimneg  15609  cbvsumv  15658  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  eirrlem  16171  lubfval  18314  glbfval  18327  odulub  18371  oduglb  18373  ablfaclem3  20064  znzrh2  21525  mplcoe3  22016  evlsval  22064  psdmul  22132  gsummoncoe1  22273  matgsum  22402  mat1f1o  22443  scmatscm  22478  mulmarep1gsum1  22538  mdettpos  22576  mp2pm2mplem4  22774  mp2pm2mplem5  22775  mp2pm2mp  22776  cpmidpmat  22838  cnmpt12f  23631  cnmptkc  23644  xkohmeo  23780  qustgpopn  24085  fsumcn  24837  ovolctb  25457  itg2monolem3  25719  dfitg  25736  itg0  25747  iblre  25761  itgreval  25764  iblconst  25785  itgconst  25786  ibladdlem  25787  itgaddlem1  25790  itgfsum  25794  iblabs  25796  itgsplit  25803  dvmptfsum  25942  dvef  25947  dvsincos  25948  dvlipcn  25961  dvfsumge  25989  coemullem  26215  dvtaylp  26335  taylthlem2  26339  pige3ALT  26484  advlogexp  26619  logtayl  26624  loglesqrt  26725  dvatan  26899  basellem2  27045  wlkson  29723  pthsfval  29787  fusgreghash2wsp  30408  rabfmpunirn  32726  psrmonprod  33696  constrcbvlem  33899  zartopn  34019  eulerpart  34526  fineqvnttrclse  35268  satf0  35554  sumeq2si  36384  prodeq2si  36386  itgeq12i  36388  cbvprodvw2  36429  neibastop2  36543  ibladdnclem  37997  itgaddnclem1  37999  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem8  38021  dvasin  38025  areacirclem1  38029  dfqmap2  38768  lshpkrlem3  39558  lcfrlem39  42027  hdmap1cbv  42248  redvmptabs  42792  mzpnegmpt  43176  mzpresrename  43182  areaquad  43644  dfid7  44039  dfrtrcl5  44056  dfrcl4  44103  fsovrfovd  44436  fsovcnvlem  44440  dssmapnvod  44447  lhe4.4ex1a  44756  dvradcnv2  44774  binomcxplemdvbinom  44780  binomcxp  44784  fprodcn  46030  limsup0  46122  dvmptfprod  46373  dvnprodlem2  46375  dvnprodlem3  46376  dvnprod  46377  iblsplit  46394  itgiccshift  46408  itgperiod  46409  stoweidlem17  46445  dirkeritg  46530  dirkercncf  46535  fourierdlem60  46594  fourierdlem61  46595  fourierdlem93  46627  fourierdlem100  46634  fourierdlem109  46643  fourierdlem112  46646  etransclem13  46675  etransclem46  46708  subsaliuncl  46786  sge0xaddlem2  46862  meaiuninc  46909  caratheodorylem1  46954  caratheodory  46956  hoicvrrex  46984  ovnsubadd  47000  sge0hsphoire  47017  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidmvle  47028  ovnhoi  47031  hspdifhsp  47044  hspmbllem3  47056  hspmbl  47057  iccvonmbl  47107  vonicc  47113  vonn0ioo  47115  vonn0icc  47116  smfadd  47193  smflimlem4  47202  smflimsuplem1  47248  smflimsup  47256  dflinc2  48886