Theorem mpteq2i 5182

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

Syntax hints:   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-mpt 5168

This theorem is referenced by:  offval22  8031  offsplitfpar  8062  konigth  10483  ofccat  14922  rlimneg  15600  cbvsumv  15649  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  eirrlem  16162  lubfval  18305  glbfval  18318  odulub  18362  oduglb  18364  ablfaclem3  20055  znzrh2  21535  mplcoe3  22026  evlsval  22074  psdmul  22142  gsummoncoe1  22283  matgsum  22412  mat1f1o  22453  scmatscm  22488  mulmarep1gsum1  22548  mdettpos  22586  mp2pm2mplem4  22784  mp2pm2mplem5  22785  mp2pm2mp  22786  cpmidpmat  22848  cnmpt12f  23641  cnmptkc  23654  xkohmeo  23790  qustgpopn  24095  fsumcn  24847  ovolctb  25467  itg2monolem3  25729  dfitg  25746  itg0  25757  iblre  25771  itgreval  25774  iblconst  25795  itgconst  25796  ibladdlem  25797  itgaddlem1  25800  itgfsum  25804  iblabs  25806  itgsplit  25813  dvmptfsum  25952  dvef  25957  dvsincos  25958  dvlipcn  25971  dvfsumge  25999  coemullem  26225  dvtaylp  26347  taylthlem2  26351  taylthlem2OLD  26352  pige3ALT  26497  advlogexp  26632  logtayl  26637  loglesqrt  26738  dvatan  26912  basellem2  27059  wlkson  29738  pthsfval  29802  fusgreghash2wsp  30423  rabfmpunirn  32741  psrmonprod  33711  constrcbvlem  33915  zartopn  34035  eulerpart  34542  fineqvnttrclse  35284  satf0  35570  sumeq2si  36400  prodeq2si  36402  itgeq12i  36404  cbvprodvw2  36445  neibastop2  36559  ibladdnclem  38011  itgaddnclem1  38013  iblabsnc  38019  iblmulc2nc  38020  ftc1anclem8  38035  dvasin  38039  areacirclem1  38043  dfqmap2  38782  lshpkrlem3  39572  lcfrlem39  42041  hdmap1cbv  42262  redvmptabs  42806  mzpnegmpt  43190  mzpresrename  43196  areaquad  43662  dfid7  44057  dfrtrcl5  44074  dfrcl4  44121  fsovrfovd  44454  fsovcnvlem  44458  dssmapnvod  44465  lhe4.4ex1a  44774  dvradcnv2  44792  binomcxplemdvbinom  44798  binomcxp  44802  fprodcn  46048  limsup0  46140  dvmptfprod  46391  dvnprodlem2  46393  dvnprodlem3  46394  dvnprod  46395  iblsplit  46412  itgiccshift  46426  itgperiod  46427  stoweidlem17  46463  dirkeritg  46548  dirkercncf  46553  fourierdlem60  46612  fourierdlem61  46613  fourierdlem93  46645  fourierdlem100  46652  fourierdlem109  46661  fourierdlem112  46664  etransclem13  46693  etransclem46  46726  subsaliuncl  46804  sge0xaddlem2  46880  meaiuninc  46927  caratheodorylem1  46972  caratheodory  46974  hoicvrrex  47002  ovnsubadd  47018  sge0hsphoire  47035  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoidmvlelem5  47045  hoidmvle  47046  ovnhoi  47049  hspdifhsp  47062  hspmbllem3  47074  hspmbl  47075  iccvonmbl  47125  vonicc  47131  vonn0ioo  47133  vonn0icc  47134  smfadd  47211  smflimlem4  47220  smflimsuplem1  47266  smflimsup  47274  dflinc2  48898