Theorem mpteq2i 5253

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

Syntax hints:   = wceq 1542   ∈ wcel 2107   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5211  df-mpt 5232

This theorem is referenced by:  offval22  8071  offsplitfpar  8102  konigth  10561  ofccat  14913  rlimneg  15590  cbvprod  15856  eirrlem  16144  lubfval  18300  glbfval  18313  odulub  18357  oduglb  18359  ablfaclem3  19952  znzrh2  21093  mplcoe3  21585  evlsval  21641  gsummoncoe1  21820  matgsum  21931  mat1f1o  21972  scmatscm  22007  mulmarep1gsum1  22067  mdettpos  22105  mp2pm2mplem4  22303  mp2pm2mplem5  22304  mp2pm2mp  22305  cpmidpmat  22367  cnmpt12f  23162  cnmptkc  23175  xkohmeo  23311  qustgpopn  23616  fsumcn  24378  ovolctb  24999  itg2monolem3  25262  dfitg  25279  itg0  25289  iblre  25303  itgreval  25306  iblconst  25327  itgconst  25328  ibladdlem  25329  itgaddlem1  25332  itgfsum  25336  iblabs  25338  itgsplit  25345  dvmptfsum  25484  dvef  25489  dvsincos  25490  dvlipcn  25503  dvfsumge  25531  coemullem  25756  dvtaylp  25874  taylthlem2  25878  pige3ALT  26021  advlogexp  26155  logtayl  26160  loglesqrt  26256  dvatan  26430  basellem2  26576  wlkson  28903  pthsfval  28968  fusgreghash2wsp  29581  rabfmpunirn  31866  zartopn  32844  eulerpart  33370  satf0  34352  neibastop2  35235  ibladdnclem  36533  itgaddnclem1  36535  iblabsnc  36541  iblmulc2nc  36542  ftc1anclem8  36557  dvasin  36561  areacirclem1  36565  lshpkrlem3  37971  lcfrlem39  40441  hdmap1cbv  40662  mzpnegmpt  41468  mzpresrename  41474  areaquad  41951  dfid7  42349  dfrtrcl5  42366  dfrcl4  42413  fsovrfovd  42746  fsovcnvlem  42750  dssmapnvod  42757  lhe4.4ex1a  43074  dvradcnv2  43092  binomcxplemdvbinom  43098  binomcxp  43102  fprodcn  44303  limsup0  44397  dvmptfprod  44648  dvnprodlem2  44650  dvnprodlem3  44651  dvnprod  44652  iblsplit  44669  itgiccshift  44683  itgperiod  44684  stoweidlem17  44720  dirkeritg  44805  dirkercncf  44810  fourierdlem60  44869  fourierdlem61  44870  fourierdlem93  44902  fourierdlem100  44909  fourierdlem109  44918  fourierdlem112  44921  etransclem13  44950  etransclem46  44983  subsaliuncl  45061  sge0xaddlem2  45137  meaiuninc  45184  caratheodorylem1  45229  caratheodory  45231  hoicvrrex  45259  ovnsubadd  45275  sge0hsphoire  45292  hoidmv1le  45297  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  hoidmvlelem5  45302  hoidmvle  45303  ovnhoi  45306  hspdifhsp  45319  hspmbllem3  45331  hspmbl  45332  iccvonmbl  45382  vonicc  45388  vonn0ioo  45390  vonn0icc  45391  smfadd  45468  smflimlem4  45477  smflimsuplem1  45523  smflimsup  45531  dflinc2  47045