Theorem mpteq2i 5191

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

Syntax hints:   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5158  df-mpt 5177

This theorem is referenced by:  offval22  8028  offsplitfpar  8059  konigth  10482  ofccat  14895  rlimneg  15573  cbvsumv  15622  cbvprod  15839  cbvprodv  15840  prodeq1i  15842  eirrlem  16132  lubfval  18273  glbfval  18286  odulub  18330  oduglb  18332  ablfaclem3  19987  znzrh2  21471  mplcoe3  21962  evlsval  22010  psdmul  22070  gsummoncoe1  22212  matgsum  22341  mat1f1o  22382  scmatscm  22417  mulmarep1gsum1  22477  mdettpos  22515  mp2pm2mplem4  22713  mp2pm2mplem5  22714  mp2pm2mp  22715  cpmidpmat  22777  cnmpt12f  23570  cnmptkc  23583  xkohmeo  23719  qustgpopn  24024  fsumcn  24778  ovolctb  25408  itg2monolem3  25670  dfitg  25687  itg0  25698  iblre  25712  itgreval  25715  iblconst  25736  itgconst  25737  ibladdlem  25738  itgaddlem1  25741  itgfsum  25745  iblabs  25747  itgsplit  25754  dvmptfsum  25896  dvef  25901  dvsincos  25902  dvlipcn  25916  dvfsumge  25945  coemullem  26172  dvtaylp  26295  taylthlem2  26299  taylthlem2OLD  26300  pige3ALT  26446  advlogexp  26581  logtayl  26586  loglesqrt  26688  dvatan  26862  basellem2  27009  wlkson  29619  pthsfval  29683  fusgreghash2wsp  30301  rabfmpunirn  32615  constrcbvlem  33741  zartopn  33861  eulerpart  34369  satf0  35364  sumeq2si  36195  prodeq2si  36197  itgeq12i  36199  cbvprodvw2  36240  neibastop2  36354  ibladdnclem  37675  itgaddnclem1  37677  iblabsnc  37683  iblmulc2nc  37684  ftc1anclem8  37699  dvasin  37703  areacirclem1  37707  lshpkrlem3  39110  lcfrlem39  41580  hdmap1cbv  41801  redvmptabs  42353  mzpnegmpt  42737  mzpresrename  42743  areaquad  43209  dfid7  43605  dfrtrcl5  43622  dfrcl4  43669  fsovrfovd  44002  fsovcnvlem  44006  dssmapnvod  44013  lhe4.4ex1a  44322  dvradcnv2  44340  binomcxplemdvbinom  44346  binomcxp  44350  fprodcn  45601  limsup0  45695  dvmptfprod  45946  dvnprodlem2  45948  dvnprodlem3  45949  dvnprod  45950  iblsplit  45967  itgiccshift  45981  itgperiod  45982  stoweidlem17  46018  dirkeritg  46103  dirkercncf  46108  fourierdlem60  46167  fourierdlem61  46168  fourierdlem93  46200  fourierdlem100  46207  fourierdlem109  46216  fourierdlem112  46219  etransclem13  46248  etransclem46  46281  subsaliuncl  46359  sge0xaddlem2  46435  meaiuninc  46482  caratheodorylem1  46527  caratheodory  46529  hoicvrrex  46557  ovnsubadd  46573  sge0hsphoire  46590  hoidmv1le  46595  hoidmvlelem1  46596  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvlelem4  46599  hoidmvlelem5  46600  hoidmvle  46601  ovnhoi  46604  hspdifhsp  46617  hspmbllem3  46629  hspmbl  46630  iccvonmbl  46680  vonicc  46686  vonn0ioo  46688  vonn0icc  46689  smfadd  46766  smflimlem4  46775  smflimsuplem1  46821  smflimsup  46829  dflinc2  48415