Theorem mpteq2i 5222

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

Syntax hints:   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-opab 5187  df-mpt 5207

This theorem is referenced by:  offval22  8092  offsplitfpar  8123  konigth  10588  ofccat  14993  rlimneg  15668  cbvsumv  15717  cbvprod  15934  cbvprodv  15935  prodeq1i  15937  eirrlem  16227  lubfval  18365  glbfval  18378  odulub  18422  oduglb  18424  ablfaclem3  20075  znzrh2  21511  mplcoe3  22001  evlsval  22049  psdmul  22109  gsummoncoe1  22251  matgsum  22380  mat1f1o  22421  scmatscm  22456  mulmarep1gsum1  22516  mdettpos  22554  mp2pm2mplem4  22752  mp2pm2mplem5  22753  mp2pm2mp  22754  cpmidpmat  22816  cnmpt12f  23609  cnmptkc  23622  xkohmeo  23758  qustgpopn  24063  fsumcn  24817  ovolctb  25448  itg2monolem3  25710  dfitg  25727  itg0  25738  iblre  25752  itgreval  25755  iblconst  25776  itgconst  25777  ibladdlem  25778  itgaddlem1  25781  itgfsum  25785  iblabs  25787  itgsplit  25794  dvmptfsum  25936  dvef  25941  dvsincos  25942  dvlipcn  25956  dvfsumge  25985  coemullem  26212  dvtaylp  26335  taylthlem2  26339  taylthlem2OLD  26340  pige3ALT  26486  advlogexp  26621  logtayl  26626  loglesqrt  26728  dvatan  26902  basellem2  27049  wlkson  29641  pthsfval  29706  fusgreghash2wsp  30324  rabfmpunirn  32636  constrcbvlem  33794  zartopn  33911  eulerpart  34419  satf0  35399  sumeq2si  36225  prodeq2si  36227  itgeq12i  36229  cbvprodvw2  36270  neibastop2  36384  ibladdnclem  37705  itgaddnclem1  37707  iblabsnc  37713  iblmulc2nc  37714  ftc1anclem8  37729  dvasin  37733  areacirclem1  37737  lshpkrlem3  39135  lcfrlem39  41605  hdmap1cbv  41826  redvmptabs  42378  mzpnegmpt  42742  mzpresrename  42748  areaquad  43215  dfid7  43611  dfrtrcl5  43628  dfrcl4  43675  fsovrfovd  44008  fsovcnvlem  44012  dssmapnvod  44019  lhe4.4ex1a  44328  dvradcnv2  44346  binomcxplemdvbinom  44352  binomcxp  44356  fprodcn  45609  limsup0  45703  dvmptfprod  45954  dvnprodlem2  45956  dvnprodlem3  45957  dvnprod  45958  iblsplit  45975  itgiccshift  45989  itgperiod  45990  stoweidlem17  46026  dirkeritg  46111  dirkercncf  46116  fourierdlem60  46175  fourierdlem61  46176  fourierdlem93  46208  fourierdlem100  46215  fourierdlem109  46224  fourierdlem112  46227  etransclem13  46256  etransclem46  46289  subsaliuncl  46367  sge0xaddlem2  46443  meaiuninc  46490  caratheodorylem1  46535  caratheodory  46537  hoicvrrex  46565  ovnsubadd  46581  sge0hsphoire  46598  hoidmv1le  46603  hoidmvlelem1  46604  hoidmvlelem2  46605  hoidmvlelem3  46606  hoidmvlelem4  46607  hoidmvlelem5  46608  hoidmvle  46609  ovnhoi  46612  hspdifhsp  46625  hspmbllem3  46637  hspmbl  46638  iccvonmbl  46688  vonicc  46694  vonn0ioo  46696  vonn0icc  46697  smfadd  46774  smflimlem4  46783  smflimsuplem1  46829  smflimsup  46837  dflinc2  48366