Theorem mpteq2i 5196

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  offval22  8040  offsplitfpar  8071  konigth  10492  ofccat  14904  rlimneg  15582  cbvsumv  15631  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  eirrlem  16141  lubfval  18283  glbfval  18296  odulub  18340  oduglb  18342  ablfaclem3  20030  znzrh2  21512  mplcoe3  22005  evlsval  22053  psdmul  22121  gsummoncoe1  22264  matgsum  22393  mat1f1o  22434  scmatscm  22469  mulmarep1gsum1  22529  mdettpos  22567  mp2pm2mplem4  22765  mp2pm2mplem5  22766  mp2pm2mp  22767  cpmidpmat  22829  cnmpt12f  23622  cnmptkc  23635  xkohmeo  23771  qustgpopn  24076  fsumcn  24829  ovolctb  25459  itg2monolem3  25721  dfitg  25738  itg0  25749  iblre  25763  itgreval  25766  iblconst  25787  itgconst  25788  ibladdlem  25789  itgaddlem1  25792  itgfsum  25796  iblabs  25798  itgsplit  25805  dvmptfsum  25947  dvef  25952  dvsincos  25953  dvlipcn  25967  dvfsumge  25996  coemullem  26223  dvtaylp  26346  taylthlem2  26350  taylthlem2OLD  26351  pige3ALT  26497  advlogexp  26632  logtayl  26637  loglesqrt  26739  dvatan  26913  basellem2  27060  wlkson  29740  pthsfval  29804  fusgreghash2wsp  30425  rabfmpunirn  32742  psrmonprod  33728  constrcbvlem  33932  zartopn  34052  eulerpart  34559  fineqvnttrclse  35299  satf0  35585  sumeq2si  36415  prodeq2si  36417  itgeq12i  36419  cbvprodvw2  36460  neibastop2  36574  ibladdnclem  37924  itgaddnclem1  37926  iblabsnc  37932  iblmulc2nc  37933  ftc1anclem8  37948  dvasin  37952  areacirclem1  37956  dfqmap2  38695  lshpkrlem3  39485  lcfrlem39  41954  hdmap1cbv  42175  redvmptabs  42727  mzpnegmpt  43098  mzpresrename  43104  areaquad  43570  dfid7  43965  dfrtrcl5  43982  dfrcl4  44029  fsovrfovd  44362  fsovcnvlem  44366  dssmapnvod  44373  lhe4.4ex1a  44682  dvradcnv2  44700  binomcxplemdvbinom  44706  binomcxp  44710  fprodcn  45957  limsup0  46049  dvmptfprod  46300  dvnprodlem2  46302  dvnprodlem3  46303  dvnprod  46304  iblsplit  46321  itgiccshift  46335  itgperiod  46336  stoweidlem17  46372  dirkeritg  46457  dirkercncf  46462  fourierdlem60  46521  fourierdlem61  46522  fourierdlem93  46554  fourierdlem100  46561  fourierdlem109  46570  fourierdlem112  46573  etransclem13  46602  etransclem46  46635  subsaliuncl  46713  sge0xaddlem2  46789  meaiuninc  46836  caratheodorylem1  46881  caratheodory  46883  hoicvrrex  46911  ovnsubadd  46927  sge0hsphoire  46944  hoidmv1le  46949  hoidmvlelem1  46950  hoidmvlelem2  46951  hoidmvlelem3  46952  hoidmvlelem4  46953  hoidmvlelem5  46954  hoidmvle  46955  ovnhoi  46958  hspdifhsp  46971  hspmbllem3  46983  hspmbl  46984  iccvonmbl  47034  vonicc  47040  vonn0ioo  47042  vonn0icc  47043  smfadd  47120  smflimlem4  47129  smflimsuplem1  47175  smflimsup  47183  dflinc2  48767