Theorem mpteq2i 5194

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

Syntax hints:   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  offval22  8030  offsplitfpar  8061  konigth  10480  ofccat  14892  rlimneg  15570  cbvsumv  15619  cbvprod  15836  cbvprodv  15837  prodeq1i  15839  eirrlem  16129  lubfval  18271  glbfval  18284  odulub  18328  oduglb  18330  ablfaclem3  20018  znzrh2  21500  mplcoe3  21993  evlsval  22041  psdmul  22109  gsummoncoe1  22252  matgsum  22381  mat1f1o  22422  scmatscm  22457  mulmarep1gsum1  22517  mdettpos  22555  mp2pm2mplem4  22753  mp2pm2mplem5  22754  mp2pm2mp  22755  cpmidpmat  22817  cnmpt12f  23610  cnmptkc  23623  xkohmeo  23759  qustgpopn  24064  fsumcn  24817  ovolctb  25447  itg2monolem3  25709  dfitg  25726  itg0  25737  iblre  25751  itgreval  25754  iblconst  25775  itgconst  25776  ibladdlem  25777  itgaddlem1  25780  itgfsum  25784  iblabs  25786  itgsplit  25793  dvmptfsum  25935  dvef  25940  dvsincos  25941  dvlipcn  25955  dvfsumge  25984  coemullem  26211  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  pige3ALT  26485  advlogexp  26620  logtayl  26625  loglesqrt  26727  dvatan  26901  basellem2  27048  wlkson  29728  pthsfval  29792  fusgreghash2wsp  30413  rabfmpunirn  32731  constrcbvlem  33912  zartopn  34032  eulerpart  34539  fineqvnttrclse  35280  satf0  35566  sumeq2si  36396  prodeq2si  36398  itgeq12i  36400  cbvprodvw2  36441  neibastop2  36555  ibladdnclem  37877  itgaddnclem1  37879  iblabsnc  37885  iblmulc2nc  37886  ftc1anclem8  37901  dvasin  37905  areacirclem1  37909  lshpkrlem3  39372  lcfrlem39  41841  hdmap1cbv  42062  redvmptabs  42615  mzpnegmpt  42986  mzpresrename  42992  areaquad  43458  dfid7  43853  dfrtrcl5  43870  dfrcl4  43917  fsovrfovd  44250  fsovcnvlem  44254  dssmapnvod  44261  lhe4.4ex1a  44570  dvradcnv2  44588  binomcxplemdvbinom  44594  binomcxp  44598  fprodcn  45846  limsup0  45938  dvmptfprod  46189  dvnprodlem2  46191  dvnprodlem3  46192  dvnprod  46193  iblsplit  46210  itgiccshift  46224  itgperiod  46225  stoweidlem17  46261  dirkeritg  46346  dirkercncf  46351  fourierdlem60  46410  fourierdlem61  46411  fourierdlem93  46443  fourierdlem100  46450  fourierdlem109  46459  fourierdlem112  46462  etransclem13  46491  etransclem46  46524  subsaliuncl  46602  sge0xaddlem2  46678  meaiuninc  46725  caratheodorylem1  46770  caratheodory  46772  hoicvrrex  46800  ovnsubadd  46816  sge0hsphoire  46833  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  hoidmvlelem5  46843  hoidmvle  46844  ovnhoi  46847  hspdifhsp  46860  hspmbllem3  46872  hspmbl  46873  iccvonmbl  46923  vonicc  46929  vonn0ioo  46931  vonn0icc  46932  smfadd  47009  smflimlem4  47018  smflimsuplem1  47064  smflimsup  47072  dflinc2  48656