Theorem mpteq2i 5209

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5194

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-mpt 5195

This theorem is used by:  offval22  8085  offsplitfpar  8116  konigth  10565  ofccat  15025  rlimneg  15717  cbvsumv  15766  cbvprod  15985  cbvprodv  15986  prodeq1i  15988  eirrlem  16277  lubfval  18421  glbfval  18434  odulub  18478  oduglb  18480  ablfaclem3  20182  znzrh2  21724  mplcoe3  22218  evlsval  22266  psdmul  22358  gsummoncoe1  22497  matgsum  22623  mat1f1o  22664  scmatscm  22699  mulmarep1gsum1  22759  mdettpos  22797  mp2pm2mplem4  22995  mp2pm2mplem5  22996  mp2pm2mp  22997  cpmidpmat  23059  cnmpt12f  23852  cnmptkc  23865  xkohmeo  24001  qustgpopn  24306  fsumcn  25058  ovolctb  25678  itg2monolem3  25940  dfitg  25957  itg0  25968  iblre  25982  itgreval  25985  iblconst  26006  itgconst  26007  ibladdlem  26008  itgaddlem1  26011  itgfsum  26015  iblabs  26017  itgsplit  26024  dvmptfsum  26163  dvef  26168  dvsincos  26169  dvlipcn  26182  dvfsumge  26210  coemullem  26436  dvtaylp  26562  taylthlem2  26566  pige3ALT  26714  advlogexp  26849  logtayl  26854  loglesqrt  26955  dvatan  27129  basellem2  27275  wlkson  30033  pthsfval  30097  fusgreghash2wsp  30718  rabfmpunirn  33027  selvply1rhmlem5  33937  selvply1rhm  33938  mplidom  33941  psrmonprod  33965  constrcbvlem  34168  zartopn  34288  eulerpart  34796  fineqvnttrclse  35553  satf0  35877  sumeq2si  36747  prodeq2si  36749  itgeq12i  36751  cbvprodvw2  36792  neibastop2  36905  ibladdnclem  38360  itgaddnclem1  38362  iblabsnc  38368  iblmulc2nc  38369  ftc1anclem8  38384  dvasin  38388  areacirclem1  38392  dfqmap2  39129  lshpkrlem3  39919  lcfrlem39  42388  hdmap1cbv  42609  redvmptabs  43154  mzpnegmpt  43508  mzpresrename  43514  areaquad  43976  dfid7  44371  dfrtrcl5  44388  dfrcl4  44435  fsovrfovd  44768  fsovcnvlem  44772  dssmapnvod  44779  lhe4.4ex1a  45072  dvradcnv2  45090  binomcxplemdvbinom  45096  binomcxp  45100  fprodcn  46349  limsup0  46441  dvmptfprod  46692  dvnprodlem2  46694  dvnprodlem3  46695  dvnprod  46696  iblsplit  46713  itgiccshift  46727  itgperiod  46728  stoweidlem17  46764  dirkeritg  46849  dirkercncf  46854  fourierdlem60  46913  fourierdlem61  46914  fourierdlem93  46946  fourierdlem100  46953  fourierdlem109  46962  fourierdlem112  46965  etransclem13  46994  etransclem46  47027  subsaliuncl  47105  sge0xaddlem2  47181  meaiuninc  47228  caratheodorylem1  47273  caratheodory  47275  hoicvrrex  47303  ovnsubadd  47319  sge0hsphoire  47336  hoidmv1le  47341  hoidmvlelem1  47342  hoidmvlelem2  47343  hoidmvlelem3  47344  hoidmvlelem4  47345  hoidmvlelem5  47346  hoidmvle  47347  ovnhoi  47350  hspdifhsp  47363  hspmbllem3  47375  hspmbl  47376  iccvonmbl  47426  vonicc  47432  vonn0ioo  47434  vonn0icc  47435  smfadd  47512  smflimlem4  47521  smflimsuplem1  47567  smflimsup  47575  dflinc2  49223