Theorem mpteq2i 5193

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

Syntax hints:   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-mpt 5179

This theorem is referenced by:  offval22  8061  offsplitfpar  8092  konigth  10521  ofccat  14976  rlimneg  15665  cbvsumv  15714  cbvprod  15934  cbvprodv  15935  prodeq1i  15937  eirrlem  16227  lubfval  18371  glbfval  18384  odulub  18428  oduglb  18430  ablfaclem3  20120  znzrh2  21585  mplcoe3  22079  evlsval  22127  psdmul  22219  gsummoncoe1  22359  matgsum  22485  mat1f1o  22526  scmatscm  22561  mulmarep1gsum1  22621  mdettpos  22659  mp2pm2mplem4  22857  mp2pm2mplem5  22858  mp2pm2mp  22859  cpmidpmat  22921  cnmpt12f  23714  cnmptkc  23727  xkohmeo  23863  qustgpopn  24168  fsumcn  24920  ovolctb  25540  itg2monolem3  25802  dfitg  25819  itg0  25830  iblre  25844  itgreval  25847  iblconst  25868  itgconst  25869  ibladdlem  25870  itgaddlem1  25873  itgfsum  25877  iblabs  25879  itgsplit  25886  dvmptfsum  26025  dvef  26030  dvsincos  26031  dvlipcn  26044  dvfsumge  26072  coemullem  26298  dvtaylp  26421  taylthlem2  26425  pige3ALT  26573  advlogexp  26708  logtayl  26713  loglesqrt  26814  dvatan  26988  basellem2  27134  wlkson  29812  pthsfval  29876  fusgreghash2wsp  30497  rabfmpunirn  32816  selvply1rhmlem5  33782  selvply1rhm  33783  mplidom  33786  psrmonprod  33810  constrcbvlem  34013  zartopn  34133  eulerpart  34640  fineqvnttrclse  35381  satf0  35683  sumeq2si  36523  prodeq2si  36525  itgeq12i  36527  cbvprodvw2  36568  neibastop2  36682  ibladdnclem  38136  itgaddnclem1  38138  iblabsnc  38144  iblmulc2nc  38145  ftc1anclem8  38160  dvasin  38164  areacirclem1  38168  dfqmap2  38907  lshpkrlem3  39697  lcfrlem39  42166  hdmap1cbv  42387  redvmptabs  42930  mzpnegmpt  43286  mzpresrename  43292  areaquad  43754  dfid7  44149  dfrtrcl5  44166  dfrcl4  44213  fsovrfovd  44546  fsovcnvlem  44550  dssmapnvod  44557  lhe4.4ex1a  44866  dvradcnv2  44884  binomcxplemdvbinom  44890  binomcxp  44894  fprodcn  46137  limsup0  46229  dvmptfprod  46480  dvnprodlem2  46482  dvnprodlem3  46483  dvnprod  46484  iblsplit  46501  itgiccshift  46515  itgperiod  46516  stoweidlem17  46552  dirkeritg  46637  dirkercncf  46642  fourierdlem60  46701  fourierdlem61  46702  fourierdlem93  46734  fourierdlem100  46741  fourierdlem109  46750  fourierdlem112  46753  etransclem13  46782  etransclem46  46815  subsaliuncl  46893  sge0xaddlem2  46969  meaiuninc  47016  caratheodorylem1  47061  caratheodory  47063  hoicvrrex  47091  ovnsubadd  47107  sge0hsphoire  47124  hoidmv1le  47129  hoidmvlelem1  47130  hoidmvlelem2  47131  hoidmvlelem3  47132  hoidmvlelem4  47133  hoidmvlelem5  47134  hoidmvle  47135  ovnhoi  47138  hspdifhsp  47151  hspmbllem3  47163  hspmbl  47164  iccvonmbl  47214  vonicc  47220  vonn0ioo  47222  vonn0icc  47223  smfadd  47300  smflimlem4  47309  smflimsuplem1  47355  smflimsup  47363  dflinc2  48993