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 1567   ∈ wcel 2149   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-mpt 5194

This theorem is referenced by:  offval22  8079  offsplitfpar  8110  konigth  10550  ofccat  15002  rlimneg  15694  cbvsumv  15743  cbvprod  15963  cbvprodv  15964  prodeq1i  15966  eirrlem  16256  lubfval  18400  glbfval  18413  odulub  18457  oduglb  18459  ablfaclem3  20155  znzrh2  21660  mplcoe3  22154  evlsval  22202  psdmul  22294  gsummoncoe1  22433  matgsum  22559  mat1f1o  22600  scmatscm  22635  mulmarep1gsum1  22695  mdettpos  22733  mp2pm2mplem4  22931  mp2pm2mplem5  22932  mp2pm2mp  22933  cpmidpmat  22995  cnmpt12f  23788  cnmptkc  23801  xkohmeo  23937  qustgpopn  24242  fsumcn  24994  ovolctb  25614  itg2monolem3  25876  dfitg  25893  itg0  25904  iblre  25918  itgreval  25921  iblconst  25942  itgconst  25943  ibladdlem  25944  itgaddlem1  25947  itgfsum  25951  iblabs  25953  itgsplit  25960  dvmptfsum  26099  dvef  26104  dvsincos  26105  dvlipcn  26118  dvfsumge  26146  coemullem  26372  dvtaylp  26495  taylthlem2  26499  pige3ALT  26647  advlogexp  26782  logtayl  26787  loglesqrt  26888  dvatan  27062  basellem2  27208  wlkson  29941  pthsfval  30005  fusgreghash2wsp  30626  rabfmpunirn  32935  selvply1rhmlem5  33855  selvply1rhm  33856  mplidom  33859  psrmonprod  33883  constrcbvlem  34086  zartopn  34206  eulerpart  34713  fineqvnttrclse  35456  satf0  35759  sumeq2si  36599  prodeq2si  36601  itgeq12i  36603  cbvprodvw2  36644  neibastop2  36757  ibladdnclem  38210  itgaddnclem1  38212  iblabsnc  38218  iblmulc2nc  38219  ftc1anclem8  38234  dvasin  38238  areacirclem1  38242  dfqmap2  38981  lshpkrlem3  39771  lcfrlem39  42240  hdmap1cbv  42461  redvmptabs  43004  mzpnegmpt  43360  mzpresrename  43366  areaquad  43828  dfid7  44223  dfrtrcl5  44240  dfrcl4  44287  fsovrfovd  44620  fsovcnvlem  44624  dssmapnvod  44631  lhe4.4ex1a  44924  dvradcnv2  44942  binomcxplemdvbinom  44948  binomcxp  44952  fprodcn  46201  limsup0  46293  dvmptfprod  46544  dvnprodlem2  46546  dvnprodlem3  46547  dvnprod  46548  iblsplit  46565  itgiccshift  46579  itgperiod  46580  stoweidlem17  46616  dirkeritg  46701  dirkercncf  46706  fourierdlem60  46765  fourierdlem61  46766  fourierdlem93  46798  fourierdlem100  46805  fourierdlem109  46814  fourierdlem112  46817  etransclem13  46846  etransclem46  46879  subsaliuncl  46957  sge0xaddlem2  47033  meaiuninc  47080  caratheodorylem1  47125  caratheodory  47127  hoicvrrex  47155  ovnsubadd  47171  sge0hsphoire  47188  hoidmv1le  47193  hoidmvlelem1  47194  hoidmvlelem2  47195  hoidmvlelem3  47196  hoidmvlelem4  47197  hoidmvlelem5  47198  hoidmvle  47199  ovnhoi  47202  hspdifhsp  47215  hspmbllem3  47227  hspmbl  47228  iccvonmbl  47278  vonicc  47284  vonn0ioo  47286  vonn0icc  47287  smfadd  47364  smflimlem4  47373  smflimsuplem1  47419  smflimsup  47427  dflinc2  49068