Theorem mpteq2i 5254

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

Syntax hints:   = wceq 1542   ∈ wcel 2107   ↦ cmpt 5232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-mpt 5233

This theorem is referenced by:  offval22  8074  offsplitfpar  8105  konigth  10564  ofccat  14916  rlimneg  15593  cbvprod  15859  eirrlem  16147  lubfval  18303  glbfval  18316  odulub  18360  oduglb  18362  ablfaclem3  19957  znzrh2  21101  mplcoe3  21593  evlsval  21649  gsummoncoe1  21828  matgsum  21939  mat1f1o  21980  scmatscm  22015  mulmarep1gsum1  22075  mdettpos  22113  mp2pm2mplem4  22311  mp2pm2mplem5  22312  mp2pm2mp  22313  cpmidpmat  22375  cnmpt12f  23170  cnmptkc  23183  xkohmeo  23319  qustgpopn  23624  fsumcn  24386  ovolctb  25007  itg2monolem3  25270  dfitg  25287  itg0  25297  iblre  25311  itgreval  25314  iblconst  25335  itgconst  25336  ibladdlem  25337  itgaddlem1  25340  itgfsum  25344  iblabs  25346  itgsplit  25353  dvmptfsum  25492  dvef  25497  dvsincos  25498  dvlipcn  25511  dvfsumge  25539  coemullem  25764  dvtaylp  25882  taylthlem2  25886  pige3ALT  26029  advlogexp  26163  logtayl  26168  loglesqrt  26266  dvatan  26440  basellem2  26586  wlkson  28913  pthsfval  28978  fusgreghash2wsp  29591  rabfmpunirn  31878  zartopn  32855  eulerpart  33381  satf0  34363  neibastop2  35246  ibladdnclem  36544  itgaddnclem1  36546  iblabsnc  36552  iblmulc2nc  36553  ftc1anclem8  36568  dvasin  36572  areacirclem1  36576  lshpkrlem3  37982  lcfrlem39  40452  hdmap1cbv  40673  mzpnegmpt  41482  mzpresrename  41488  areaquad  41965  dfid7  42363  dfrtrcl5  42380  dfrcl4  42427  fsovrfovd  42760  fsovcnvlem  42764  dssmapnvod  42771  lhe4.4ex1a  43088  dvradcnv2  43106  binomcxplemdvbinom  43112  binomcxp  43116  fprodcn  44316  limsup0  44410  dvmptfprod  44661  dvnprodlem2  44663  dvnprodlem3  44664  dvnprod  44665  iblsplit  44682  itgiccshift  44696  itgperiod  44697  stoweidlem17  44733  dirkeritg  44818  dirkercncf  44823  fourierdlem60  44882  fourierdlem61  44883  fourierdlem93  44915  fourierdlem100  44922  fourierdlem109  44931  fourierdlem112  44934  etransclem13  44963  etransclem46  44996  subsaliuncl  45074  sge0xaddlem2  45150  meaiuninc  45197  caratheodorylem1  45242  caratheodory  45244  hoicvrrex  45272  ovnsubadd  45288  sge0hsphoire  45305  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  hoidmvlelem5  45315  hoidmvle  45316  ovnhoi  45319  hspdifhsp  45332  hspmbllem3  45344  hspmbl  45345  iccvonmbl  45395  vonicc  45401  vonn0ioo  45403  vonn0icc  45404  smfadd  45481  smflimlem4  45490  smflimsuplem1  45536  smflimsup  45544  dflinc2  47091