Theorem mpteq2i 5201

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  offval22  8097  offsplitfpar  8128  konigth  10647  ofccat  15115  rlimneg  15807  cbvsumv  15856  cbvprod  16075  cbvprodv  16076  prodeq1i  16078  eirrlem  16365  lubfval  18515  glbfval  18528  odulub  18572  oduglb  18574  ablfaclem3  20296  znzrh2  21844  mplcoe3  22340  evlsval  22388  psdmul  22480  gsummoncoe1  22619  matgsum  22745  mat1f1o  22786  scmatscm  22821  mulmarep1gsum1  22881  mdettpos  22919  mp2pm2mplem4  23120  mp2pm2mplem5  23121  mp2pm2mp  23122  cpmidpmat  23184  cnmpt12f  23978  cnmptkc  23991  xkohmeo  24127  qustgpopn  24432  fsumcn  25184  ovolctb  25804  itg2monolem3  26066  dfitg  26083  itg0  26093  iblre  26107  itgreval  26110  iblconst  26131  itgconst  26132  ibladdlem  26133  itgaddlem1  26136  itgfsum  26140  iblabs  26142  itgsplit  26149  dvmptfsum  26288  dvef  26293  dvsincos  26294  dvlipcn  26307  dvfsumge  26335  coemullem  26562  dvtaylp  26690  taylthlem2  26694  pige3ALT  26841  advlogexp  26976  logtayl  26981  loglesqrt  27082  dvatan  27256  basellem2  27402  wlkson  30228  pthsfval  30297  fusgreghash2wsp  30932  rabfmpunirn  33240  selvply1rhmlem5  34149  selvply1rhm  34150  mplidom  34153  psrmonprod  34177  constrcbvlem  34380  zartopn  34500  eulerpart  35007  fineqvnttrclse  35775  satf0  36116  sumeq2si  36971  prodeq2si  36973  itgeq12i  36975  cbvprodvw2  37016  neibastop2  37129  ibladdnclem  38574  itgaddnclem1  38576  iblabsnc  38582  iblmulc2nc  38583  ftc1anclem8  38598  dvasin  38602  areacirclem1  38606  dfqmap2  39359  lshpkrlem3  40149  lcfrlem39  42618  hdmap1cbv  42839  redvmptabs  43391  mzpnegmpt  43734  mzpresrename  43740  areaquad  44202  dfid7  44597  dfrtrcl5  44614  dfrcl4  44661  fsovrfovd  44994  fsovcnvlem  44998  dssmapnvod  45005  lhe4.4ex1a  45298  dvradcnv2  45316  binomcxplemdvbinom  45322  binomcxp  45326  fprodcn  46581  limsup0  46673  dvmptfprod  46924  dvnprodlem2  46926  dvnprodlem3  46927  dvnprod  46928  iblsplit  46945  itgiccshift  46959  itgperiod  46960  stoweidlem17  46996  dirkeritg  47081  dirkercncf  47086  fourierdlem60  47145  fourierdlem61  47146  fourierdlem93  47178  fourierdlem100  47185  fourierdlem109  47194  fourierdlem112  47197  etransclem13  47226  etransclem46  47259  subsaliuncl  47337  sge0xaddlem2  47413  meaiuninc  47460  caratheodorylem1  47505  caratheodory  47507  hoicvrrex  47535  ovnsubadd  47551  sge0hsphoire  47568  hoidmv1le  47573  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvlelem4  47577  hoidmvlelem5  47578  hoidmvle  47579  ovnhoi  47582  hspdifhsp  47595  hspmbllem3  47607  hspmbl  47608  iccvonmbl  47658  vonicc  47664  vonn0ioo  47666  vonn0icc  47667  smfadd  47744  smflimlem4  47753  smflimsuplem1  47799  smflimsup  47807  dflinc2  49491  veroquadmodzerod  50953