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 1541   ∈ wcel 2111   ↦ cmpt 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5149  df-mpt 5168

This theorem is referenced by:  offval22  8013  offsplitfpar  8044  konigth  10455  ofccat  14871  rlimneg  15549  cbvsumv  15598  cbvprod  15815  cbvprodv  15816  prodeq1i  15818  eirrlem  16108  lubfval  18249  glbfval  18262  odulub  18306  oduglb  18308  ablfaclem3  19996  znzrh2  21477  mplcoe3  21968  evlsval  22016  psdmul  22076  gsummoncoe1  22218  matgsum  22347  mat1f1o  22388  scmatscm  22423  mulmarep1gsum1  22483  mdettpos  22521  mp2pm2mplem4  22719  mp2pm2mplem5  22720  mp2pm2mp  22721  cpmidpmat  22783  cnmpt12f  23576  cnmptkc  23589  xkohmeo  23725  qustgpopn  24030  fsumcn  24783  ovolctb  25413  itg2monolem3  25675  dfitg  25692  itg0  25703  iblre  25717  itgreval  25720  iblconst  25741  itgconst  25742  ibladdlem  25743  itgaddlem1  25746  itgfsum  25750  iblabs  25752  itgsplit  25759  dvmptfsum  25901  dvef  25906  dvsincos  25907  dvlipcn  25921  dvfsumge  25950  coemullem  26177  dvtaylp  26300  taylthlem2  26304  taylthlem2OLD  26305  pige3ALT  26451  advlogexp  26586  logtayl  26591  loglesqrt  26693  dvatan  26867  basellem2  27014  wlkson  29628  pthsfval  29692  fusgreghash2wsp  30310  rabfmpunirn  32627  constrcbvlem  33760  zartopn  33880  eulerpart  34387  fineqvnttrclse  35136  satf0  35408  sumeq2si  36236  prodeq2si  36238  itgeq12i  36240  cbvprodvw2  36281  neibastop2  36395  ibladdnclem  37716  itgaddnclem1  37718  iblabsnc  37724  iblmulc2nc  37725  ftc1anclem8  37740  dvasin  37744  areacirclem1  37748  lshpkrlem3  39151  lcfrlem39  41620  hdmap1cbv  41841  redvmptabs  42393  mzpnegmpt  42777  mzpresrename  42783  areaquad  43249  dfid7  43645  dfrtrcl5  43662  dfrcl4  43709  fsovrfovd  44042  fsovcnvlem  44046  dssmapnvod  44053  lhe4.4ex1a  44362  dvradcnv2  44380  binomcxplemdvbinom  44386  binomcxp  44390  fprodcn  45640  limsup0  45732  dvmptfprod  45983  dvnprodlem2  45985  dvnprodlem3  45986  dvnprod  45987  iblsplit  46004  itgiccshift  46018  itgperiod  46019  stoweidlem17  46055  dirkeritg  46140  dirkercncf  46145  fourierdlem60  46204  fourierdlem61  46205  fourierdlem93  46237  fourierdlem100  46244  fourierdlem109  46253  fourierdlem112  46256  etransclem13  46285  etransclem46  46318  subsaliuncl  46396  sge0xaddlem2  46472  meaiuninc  46519  caratheodorylem1  46564  caratheodory  46566  hoicvrrex  46594  ovnsubadd  46610  sge0hsphoire  46627  hoidmv1le  46632  hoidmvlelem1  46633  hoidmvlelem2  46634  hoidmvlelem3  46635  hoidmvlelem4  46636  hoidmvlelem5  46637  hoidmvle  46638  ovnhoi  46641  hspdifhsp  46654  hspmbllem3  46666  hspmbl  46667  iccvonmbl  46717  vonicc  46723  vonn0ioo  46725  vonn0icc  46726  smfadd  46803  smflimlem4  46812  smflimsuplem1  46858  smflimsup  46866  dflinc2  48442