Theorem mpteq2i 5271

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

Syntax hints:   = wceq 1537   ∈ wcel 2108   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  offval22  8129  offsplitfpar  8160  konigth  10638  ofccat  15018  rlimneg  15695  cbvsumv  15744  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  eirrlem  16252  lubfval  18420  glbfval  18433  odulub  18477  oduglb  18479  ablfaclem3  20131  znzrh2  21587  mplcoe3  22079  evlsval  22133  psdmul  22193  gsummoncoe1  22333  matgsum  22464  mat1f1o  22505  scmatscm  22540  mulmarep1gsum1  22600  mdettpos  22638  mp2pm2mplem4  22836  mp2pm2mplem5  22837  mp2pm2mp  22838  cpmidpmat  22900  cnmpt12f  23695  cnmptkc  23708  xkohmeo  23844  qustgpopn  24149  fsumcn  24913  ovolctb  25544  itg2monolem3  25807  dfitg  25824  itg0  25835  iblre  25849  itgreval  25852  iblconst  25873  itgconst  25874  ibladdlem  25875  itgaddlem1  25878  itgfsum  25882  iblabs  25884  itgsplit  25891  dvmptfsum  26033  dvef  26038  dvsincos  26039  dvlipcn  26053  dvfsumge  26082  coemullem  26309  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  pige3ALT  26580  advlogexp  26715  logtayl  26720  loglesqrt  26822  dvatan  26996  basellem2  27143  wlkson  29692  pthsfval  29757  fusgreghash2wsp  30370  rabfmpunirn  32671  zartopn  33821  eulerpart  34347  satf0  35340  sumeq2si  36166  prodeq2si  36168  itgeq12i  36170  cbvprodvw2  36213  neibastop2  36327  ibladdnclem  37636  itgaddnclem1  37638  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem8  37660  dvasin  37664  areacirclem1  37668  lshpkrlem3  39068  lcfrlem39  41538  hdmap1cbv  41759  mzpnegmpt  42700  mzpresrename  42706  areaquad  43177  dfid7  43574  dfrtrcl5  43591  dfrcl4  43638  fsovrfovd  43971  fsovcnvlem  43975  dssmapnvod  43982  lhe4.4ex1a  44298  dvradcnv2  44316  binomcxplemdvbinom  44322  binomcxp  44326  fprodcn  45521  limsup0  45615  dvmptfprod  45866  dvnprodlem2  45868  dvnprodlem3  45869  dvnprod  45870  iblsplit  45887  itgiccshift  45901  itgperiod  45902  stoweidlem17  45938  dirkeritg  46023  dirkercncf  46028  fourierdlem60  46087  fourierdlem61  46088  fourierdlem93  46120  fourierdlem100  46127  fourierdlem109  46136  fourierdlem112  46139  etransclem13  46168  etransclem46  46201  subsaliuncl  46279  sge0xaddlem2  46355  meaiuninc  46402  caratheodorylem1  46447  caratheodory  46449  hoicvrrex  46477  ovnsubadd  46493  sge0hsphoire  46510  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hoidmvle  46521  ovnhoi  46524  hspdifhsp  46537  hspmbllem3  46549  hspmbl  46550  iccvonmbl  46600  vonicc  46606  vonn0ioo  46608  vonn0icc  46609  smfadd  46686  smflimlem4  46695  smflimsuplem1  46741  smflimsup  46749  dflinc2  48139