Theorem mpteq2i 5122

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

Syntax hints:   = wceq 1538   ∈ wcel 2111   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  offval22  7766  offsplitfpar  7798  konigth  9980  ofccat  14320  rlimneg  14995  cbvprod  15261  eirrlem  15549  lubfval  17580  glbfval  17593  oduglb  17741  odulub  17743  ablfaclem3  19202  znzrh2  20237  mplcoe3  20706  evlsval  20758  gsummoncoe1  20933  matgsum  21042  mat1f1o  21083  scmatscm  21118  mulmarep1gsum1  21178  mdettpos  21216  mp2pm2mplem4  21414  mp2pm2mplem5  21415  mp2pm2mp  21416  cpmidpmat  21478  cnmpt12f  22271  cnmptkc  22284  xkohmeo  22420  qustgpopn  22725  fsumcn  23475  ovolctb  24094  itg2monolem3  24356  dfitg  24373  itg0  24383  iblre  24397  itgreval  24400  iblconst  24421  itgconst  24422  ibladdlem  24423  itgaddlem1  24426  itgfsum  24430  iblabs  24432  itgsplit  24439  dvmptfsum  24578  dvef  24583  dvsincos  24584  dvlipcn  24597  dvfsumge  24625  coemullem  24847  dvtaylp  24965  taylthlem2  24969  pige3ALT  25112  advlogexp  25246  logtayl  25251  loglesqrt  25347  dvatan  25521  basellem2  25667  wlkson  27446  pthsfval  27510  fusgreghash2wsp  28123  rabfmpunirn  30416  zartopn  31228  eulerpart  31750  satf0  32732  trpredlem1  33179  trpred0  33188  neibastop2  33822  ibladdnclem  35113  itgaddnclem1  35115  iblabsnc  35121  iblmulc2nc  35122  ftc1anclem8  35137  dvasin  35141  areacirclem1  35145  lshpkrlem3  36408  lcfrlem39  38877  hdmap1cbv  39098  mzpnegmpt  39685  mzpresrename  39691  areaquad  40166  dfid7  40312  dfrtrcl5  40329  dfrcl4  40377  fsovrfovd  40710  fsovcnvlem  40714  dssmapnvod  40721  lhe4.4ex1a  41033  dvradcnv2  41051  binomcxplemdvbinom  41057  binomcxp  41061  fprodcn  42242  limsup0  42336  dvmptfprod  42587  dvnprodlem2  42589  dvnprodlem3  42590  dvnprod  42591  iblsplit  42608  itgiccshift  42622  itgperiod  42623  stoweidlem17  42659  dirkeritg  42744  dirkercncf  42749  fourierdlem60  42808  fourierdlem61  42809  fourierdlem93  42841  fourierdlem100  42848  fourierdlem109  42857  fourierdlem112  42860  etransclem13  42889  etransclem46  42922  subsaliuncl  42998  sge0xaddlem2  43073  meaiuninc  43120  caratheodorylem1  43165  caratheodory  43167  hoicvrrex  43195  ovnsubadd  43211  sge0hsphoire  43228  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoidmvlelem5  43238  hoidmvle  43239  ovnhoi  43242  hspdifhsp  43255  hspmbllem3  43267  hspmbl  43268  iccvonmbl  43318  vonicc  43324  vonn0ioo  43326  vonn0icc  43327  smfadd  43398  smflimlem4  43407  smflimsuplem1  43451  smflimsup  43459  dflinc2  44819