Theorem mpteq2i 5252

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

Syntax hints:   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-mpt 5231

This theorem is referenced by:  offval22  8111  offsplitfpar  8142  konigth  10606  ofccat  15004  rlimneg  15679  cbvsumv  15728  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  eirrlem  16236  lubfval  18407  glbfval  18420  odulub  18464  oduglb  18466  ablfaclem3  20121  znzrh2  21581  mplcoe3  22073  evlsval  22127  psdmul  22187  gsummoncoe1  22327  matgsum  22458  mat1f1o  22499  scmatscm  22534  mulmarep1gsum1  22594  mdettpos  22632  mp2pm2mplem4  22830  mp2pm2mplem5  22831  mp2pm2mp  22832  cpmidpmat  22894  cnmpt12f  23689  cnmptkc  23702  xkohmeo  23838  qustgpopn  24143  fsumcn  24907  ovolctb  25538  itg2monolem3  25801  dfitg  25818  itg0  25829  iblre  25843  itgreval  25846  iblconst  25867  itgconst  25868  ibladdlem  25869  itgaddlem1  25872  itgfsum  25876  iblabs  25878  itgsplit  25885  dvmptfsum  26027  dvef  26032  dvsincos  26033  dvlipcn  26047  dvfsumge  26076  coemullem  26303  dvtaylp  26426  taylthlem2  26430  taylthlem2OLD  26431  pige3ALT  26576  advlogexp  26711  logtayl  26716  loglesqrt  26818  dvatan  26992  basellem2  27139  wlkson  29688  pthsfval  29753  fusgreghash2wsp  30366  rabfmpunirn  32669  zartopn  33835  eulerpart  34363  satf0  35356  sumeq2si  36183  prodeq2si  36185  itgeq12i  36187  cbvprodvw2  36229  neibastop2  36343  ibladdnclem  37662  itgaddnclem1  37664  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem8  37686  dvasin  37690  areacirclem1  37694  lshpkrlem3  39093  lcfrlem39  41563  hdmap1cbv  41784  redvmptabs  42368  mzpnegmpt  42731  mzpresrename  42737  areaquad  43204  dfid7  43601  dfrtrcl5  43618  dfrcl4  43665  fsovrfovd  43998  fsovcnvlem  44002  dssmapnvod  44009  lhe4.4ex1a  44324  dvradcnv2  44342  binomcxplemdvbinom  44348  binomcxp  44352  fprodcn  45555  limsup0  45649  dvmptfprod  45900  dvnprodlem2  45902  dvnprodlem3  45903  dvnprod  45904  iblsplit  45921  itgiccshift  45935  itgperiod  45936  stoweidlem17  45972  dirkeritg  46057  dirkercncf  46062  fourierdlem60  46121  fourierdlem61  46122  fourierdlem93  46154  fourierdlem100  46161  fourierdlem109  46170  fourierdlem112  46173  etransclem13  46202  etransclem46  46235  subsaliuncl  46313  sge0xaddlem2  46389  meaiuninc  46436  caratheodorylem1  46481  caratheodory  46483  hoicvrrex  46511  ovnsubadd  46527  sge0hsphoire  46544  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvlelem5  46554  hoidmvle  46555  ovnhoi  46558  hspdifhsp  46571  hspmbllem3  46583  hspmbl  46584  iccvonmbl  46634  vonicc  46640  vonn0ioo  46642  vonn0icc  46643  smfadd  46720  smflimlem4  46729  smflimsuplem1  46775  smflimsup  46783  dflinc2  48255