Theorem mpteq2i 5208

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

Syntax hints:   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-mpt 5194

This theorem is referenced by:  offval22  8084  offsplitfpar  8115  konigth  10555  ofccat  15008  rlimneg  15700  cbvsumv  15749  cbvprod  15969  cbvprodv  15970  prodeq1i  15972  eirrlem  16261  lubfval  18405  glbfval  18418  odulub  18462  oduglb  18464  ablfaclem3  20160  znzrh2  21676  mplcoe3  22170  evlsval  22218  psdmul  22310  gsummoncoe1  22449  matgsum  22575  mat1f1o  22616  scmatscm  22651  mulmarep1gsum1  22711  mdettpos  22749  mp2pm2mplem4  22947  mp2pm2mplem5  22948  mp2pm2mp  22949  cpmidpmat  23011  cnmpt12f  23804  cnmptkc  23817  xkohmeo  23953  qustgpopn  24258  fsumcn  25010  ovolctb  25630  itg2monolem3  25892  dfitg  25909  itg0  25920  iblre  25934  itgreval  25937  iblconst  25958  itgconst  25959  ibladdlem  25960  itgaddlem1  25963  itgfsum  25967  iblabs  25969  itgsplit  25976  dvmptfsum  26115  dvef  26120  dvsincos  26121  dvlipcn  26134  dvfsumge  26162  coemullem  26388  dvtaylp  26514  taylthlem2  26518  pige3ALT  26666  advlogexp  26801  logtayl  26806  loglesqrt  26907  dvatan  27081  basellem2  27227  wlkson  29985  pthsfval  30049  fusgreghash2wsp  30670  rabfmpunirn  32979  selvply1rhmlem5  33895  selvply1rhm  33896  mplidom  33899  psrmonprod  33923  constrcbvlem  34126  zartopn  34246  eulerpart  34753  fineqvnttrclse  35518  satf0  35845  sumeq2si  36695  prodeq2si  36697  itgeq12i  36699  cbvprodvw2  36740  neibastop2  36853  ibladdnclem  38308  itgaddnclem1  38310  iblabsnc  38316  iblmulc2nc  38317  ftc1anclem8  38332  dvasin  38336  areacirclem1  38340  dfqmap2  39077  lshpkrlem3  39867  lcfrlem39  42336  hdmap1cbv  42557  redvmptabs  43102  mzpnegmpt  43458  mzpresrename  43464  areaquad  43926  dfid7  44321  dfrtrcl5  44338  dfrcl4  44385  fsovrfovd  44718  fsovcnvlem  44722  dssmapnvod  44729  lhe4.4ex1a  45022  dvradcnv2  45040  binomcxplemdvbinom  45046  binomcxp  45050  fprodcn  46299  limsup0  46391  dvmptfprod  46642  dvnprodlem2  46644  dvnprodlem3  46645  dvnprod  46646  iblsplit  46663  itgiccshift  46677  itgperiod  46678  stoweidlem17  46714  dirkeritg  46799  dirkercncf  46804  fourierdlem60  46863  fourierdlem61  46864  fourierdlem93  46896  fourierdlem100  46903  fourierdlem109  46912  fourierdlem112  46915  etransclem13  46944  etransclem46  46977  subsaliuncl  47055  sge0xaddlem2  47131  meaiuninc  47178  caratheodorylem1  47223  caratheodory  47225  hoicvrrex  47253  ovnsubadd  47269  sge0hsphoire  47286  hoidmv1le  47291  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvlelem4  47295  hoidmvlelem5  47296  hoidmvle  47297  ovnhoi  47300  hspdifhsp  47313  hspmbllem3  47325  hspmbl  47326  iccvonmbl  47376  vonicc  47382  vonn0ioo  47384  vonn0icc  47385  smfadd  47462  smflimlem4  47471  smflimsuplem1  47517  smflimsup  47525  dflinc2  49173