Theorem mpteq2i 5203

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

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

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 5170  df-mpt 5189

This theorem is referenced by:  offval22  8067  offsplitfpar  8098  konigth  10522  ofccat  14935  rlimneg  15613  cbvsumv  15662  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  eirrlem  16172  lubfval  18309  glbfval  18322  odulub  18366  oduglb  18368  ablfaclem3  20019  znzrh2  21455  mplcoe3  21945  evlsval  21993  psdmul  22053  gsummoncoe1  22195  matgsum  22324  mat1f1o  22365  scmatscm  22400  mulmarep1gsum1  22460  mdettpos  22498  mp2pm2mplem4  22696  mp2pm2mplem5  22697  mp2pm2mp  22698  cpmidpmat  22760  cnmpt12f  23553  cnmptkc  23566  xkohmeo  23702  qustgpopn  24007  fsumcn  24761  ovolctb  25391  itg2monolem3  25653  dfitg  25670  itg0  25681  iblre  25695  itgreval  25698  iblconst  25719  itgconst  25720  ibladdlem  25721  itgaddlem1  25724  itgfsum  25728  iblabs  25730  itgsplit  25737  dvmptfsum  25879  dvef  25884  dvsincos  25885  dvlipcn  25899  dvfsumge  25928  coemullem  26155  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  pige3ALT  26429  advlogexp  26564  logtayl  26569  loglesqrt  26671  dvatan  26845  basellem2  26992  wlkson  29584  pthsfval  29649  fusgreghash2wsp  30267  rabfmpunirn  32577  constrcbvlem  33745  zartopn  33865  eulerpart  34373  satf0  35359  sumeq2si  36190  prodeq2si  36192  itgeq12i  36194  cbvprodvw2  36235  neibastop2  36349  ibladdnclem  37670  itgaddnclem1  37672  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem8  37694  dvasin  37698  areacirclem1  37702  lshpkrlem3  39105  lcfrlem39  41575  hdmap1cbv  41796  redvmptabs  42348  mzpnegmpt  42732  mzpresrename  42738  areaquad  43205  dfid7  43601  dfrtrcl5  43618  dfrcl4  43665  fsovrfovd  43998  fsovcnvlem  44002  dssmapnvod  44009  lhe4.4ex1a  44318  dvradcnv2  44336  binomcxplemdvbinom  44342  binomcxp  44346  fprodcn  45598  limsup0  45692  dvmptfprod  45943  dvnprodlem2  45945  dvnprodlem3  45946  dvnprod  45947  iblsplit  45964  itgiccshift  45978  itgperiod  45979  stoweidlem17  46015  dirkeritg  46100  dirkercncf  46105  fourierdlem60  46164  fourierdlem61  46165  fourierdlem93  46197  fourierdlem100  46204  fourierdlem109  46213  fourierdlem112  46216  etransclem13  46245  etransclem46  46278  subsaliuncl  46356  sge0xaddlem2  46432  meaiuninc  46479  caratheodorylem1  46524  caratheodory  46526  hoicvrrex  46554  ovnsubadd  46570  sge0hsphoire  46587  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hoidmvle  46598  ovnhoi  46601  hspdifhsp  46614  hspmbllem3  46626  hspmbl  46627  iccvonmbl  46677  vonicc  46683  vonn0ioo  46685  vonn0icc  46686  smfadd  46763  smflimlem4  46772  smflimsuplem1  46818  smflimsup  46826  dflinc2  48399