Theorem mpteq2i 5198

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

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

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 5165  df-mpt 5184

This theorem is referenced by:  offval22  8044  offsplitfpar  8075  konigth  10498  ofccat  14911  rlimneg  15589  cbvsumv  15638  cbvprod  15855  cbvprodv  15856  prodeq1i  15858  eirrlem  16148  lubfval  18285  glbfval  18298  odulub  18342  oduglb  18344  ablfaclem3  19995  znzrh2  21431  mplcoe3  21921  evlsval  21969  psdmul  22029  gsummoncoe1  22171  matgsum  22300  mat1f1o  22341  scmatscm  22376  mulmarep1gsum1  22436  mdettpos  22474  mp2pm2mplem4  22672  mp2pm2mplem5  22673  mp2pm2mp  22674  cpmidpmat  22736  cnmpt12f  23529  cnmptkc  23542  xkohmeo  23678  qustgpopn  23983  fsumcn  24737  ovolctb  25367  itg2monolem3  25629  dfitg  25646  itg0  25657  iblre  25671  itgreval  25674  iblconst  25695  itgconst  25696  ibladdlem  25697  itgaddlem1  25700  itgfsum  25704  iblabs  25706  itgsplit  25713  dvmptfsum  25855  dvef  25860  dvsincos  25861  dvlipcn  25875  dvfsumge  25904  coemullem  26131  dvtaylp  26254  taylthlem2  26258  taylthlem2OLD  26259  pige3ALT  26405  advlogexp  26540  logtayl  26545  loglesqrt  26647  dvatan  26821  basellem2  26968  wlkson  29558  pthsfval  29622  fusgreghash2wsp  30240  rabfmpunirn  32550  constrcbvlem  33718  zartopn  33838  eulerpart  34346  satf0  35332  sumeq2si  36163  prodeq2si  36165  itgeq12i  36167  cbvprodvw2  36208  neibastop2  36322  ibladdnclem  37643  itgaddnclem1  37645  iblabsnc  37651  iblmulc2nc  37652  ftc1anclem8  37667  dvasin  37671  areacirclem1  37675  lshpkrlem3  39078  lcfrlem39  41548  hdmap1cbv  41769  redvmptabs  42321  mzpnegmpt  42705  mzpresrename  42711  areaquad  43178  dfid7  43574  dfrtrcl5  43591  dfrcl4  43638  fsovrfovd  43971  fsovcnvlem  43975  dssmapnvod  43982  lhe4.4ex1a  44291  dvradcnv2  44309  binomcxplemdvbinom  44315  binomcxp  44319  fprodcn  45571  limsup0  45665  dvmptfprod  45916  dvnprodlem2  45918  dvnprodlem3  45919  dvnprod  45920  iblsplit  45937  itgiccshift  45951  itgperiod  45952  stoweidlem17  45988  dirkeritg  46073  dirkercncf  46078  fourierdlem60  46137  fourierdlem61  46138  fourierdlem93  46170  fourierdlem100  46177  fourierdlem109  46186  fourierdlem112  46189  etransclem13  46218  etransclem46  46251  subsaliuncl  46329  sge0xaddlem2  46405  meaiuninc  46452  caratheodorylem1  46497  caratheodory  46499  hoicvrrex  46527  ovnsubadd  46543  sge0hsphoire  46560  hoidmv1le  46565  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  hoidmvlelem5  46570  hoidmvle  46571  ovnhoi  46574  hspdifhsp  46587  hspmbllem3  46599  hspmbl  46600  iccvonmbl  46650  vonicc  46656  vonn0ioo  46658  vonn0icc  46659  smfadd  46736  smflimlem4  46745  smflimsuplem1  46791  smflimsup  46799  dflinc2  48372