Theorem mpteq2i 5247

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

Syntax hints:   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5225

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226

This theorem is referenced by:  offval22  8113  offsplitfpar  8144  konigth  10609  ofccat  15008  rlimneg  15683  cbvsumv  15732  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  eirrlem  16240  lubfval  18395  glbfval  18408  odulub  18452  oduglb  18454  ablfaclem3  20107  znzrh2  21564  mplcoe3  22056  evlsval  22110  psdmul  22170  gsummoncoe1  22312  matgsum  22443  mat1f1o  22484  scmatscm  22519  mulmarep1gsum1  22579  mdettpos  22617  mp2pm2mplem4  22815  mp2pm2mplem5  22816  mp2pm2mp  22817  cpmidpmat  22879  cnmpt12f  23674  cnmptkc  23687  xkohmeo  23823  qustgpopn  24128  fsumcn  24894  ovolctb  25525  itg2monolem3  25787  dfitg  25804  itg0  25815  iblre  25829  itgreval  25832  iblconst  25853  itgconst  25854  ibladdlem  25855  itgaddlem1  25858  itgfsum  25862  iblabs  25864  itgsplit  25871  dvmptfsum  26013  dvef  26018  dvsincos  26019  dvlipcn  26033  dvfsumge  26062  coemullem  26289  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  pige3ALT  26562  advlogexp  26697  logtayl  26702  loglesqrt  26804  dvatan  26978  basellem2  27125  wlkson  29674  pthsfval  29739  fusgreghash2wsp  30357  rabfmpunirn  32663  zartopn  33874  eulerpart  34384  satf0  35377  sumeq2si  36203  prodeq2si  36205  itgeq12i  36207  cbvprodvw2  36248  neibastop2  36362  ibladdnclem  37683  itgaddnclem1  37685  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem8  37707  dvasin  37711  areacirclem1  37715  lshpkrlem3  39113  lcfrlem39  41583  hdmap1cbv  41804  redvmptabs  42390  mzpnegmpt  42755  mzpresrename  42761  areaquad  43228  dfid7  43625  dfrtrcl5  43642  dfrcl4  43689  fsovrfovd  44022  fsovcnvlem  44026  dssmapnvod  44033  lhe4.4ex1a  44348  dvradcnv2  44366  binomcxplemdvbinom  44372  binomcxp  44376  fprodcn  45615  limsup0  45709  dvmptfprod  45960  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  iblsplit  45981  itgiccshift  45995  itgperiod  45996  stoweidlem17  46032  dirkeritg  46117  dirkercncf  46122  fourierdlem60  46181  fourierdlem61  46182  fourierdlem93  46214  fourierdlem100  46221  fourierdlem109  46230  fourierdlem112  46233  etransclem13  46262  etransclem46  46295  subsaliuncl  46373  sge0xaddlem2  46449  meaiuninc  46496  caratheodorylem1  46541  caratheodory  46543  hoicvrrex  46571  ovnsubadd  46587  sge0hsphoire  46604  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hoidmvle  46615  ovnhoi  46618  hspdifhsp  46631  hspmbllem3  46643  hspmbl  46644  iccvonmbl  46694  vonicc  46700  vonn0ioo  46702  vonn0icc  46703  smfadd  46780  smflimlem4  46789  smflimsuplem1  46835  smflimsup  46843  dflinc2  48327