Theorem mpteq2i 5191

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

Syntax hints:   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5176

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-mpt 5177

This theorem is referenced by:  offval22  8027  offsplitfpar  8058  konigth  10471  ofccat  14883  rlimneg  15561  cbvsumv  15610  cbvprod  15827  cbvprodv  15828  prodeq1i  15830  eirrlem  16120  lubfval  18262  glbfval  18275  odulub  18319  oduglb  18321  ablfaclem3  20009  znzrh2  21491  mplcoe3  21984  evlsval  22032  psdmul  22100  gsummoncoe1  22243  matgsum  22372  mat1f1o  22413  scmatscm  22448  mulmarep1gsum1  22508  mdettpos  22546  mp2pm2mplem4  22744  mp2pm2mplem5  22745  mp2pm2mp  22746  cpmidpmat  22808  cnmpt12f  23601  cnmptkc  23614  xkohmeo  23750  qustgpopn  24055  fsumcn  24808  ovolctb  25438  itg2monolem3  25700  dfitg  25717  itg0  25728  iblre  25742  itgreval  25745  iblconst  25766  itgconst  25767  ibladdlem  25768  itgaddlem1  25771  itgfsum  25775  iblabs  25777  itgsplit  25784  dvmptfsum  25926  dvef  25931  dvsincos  25932  dvlipcn  25946  dvfsumge  25975  coemullem  26202  dvtaylp  26325  taylthlem2  26329  taylthlem2OLD  26330  pige3ALT  26476  advlogexp  26611  logtayl  26616  loglesqrt  26718  dvatan  26892  basellem2  27039  wlkson  29654  pthsfval  29718  fusgreghash2wsp  30339  rabfmpunirn  32657  constrcbvlem  33840  zartopn  33960  eulerpart  34467  fineqvnttrclse  35216  satf0  35488  sumeq2si  36318  prodeq2si  36320  itgeq12i  36322  cbvprodvw2  36363  neibastop2  36477  ibladdnclem  37789  itgaddnclem1  37791  iblabsnc  37797  iblmulc2nc  37798  ftc1anclem8  37813  dvasin  37817  areacirclem1  37821  lshpkrlem3  39284  lcfrlem39  41753  hdmap1cbv  41974  redvmptabs  42530  mzpnegmpt  42901  mzpresrename  42907  areaquad  43373  dfid7  43769  dfrtrcl5  43786  dfrcl4  43833  fsovrfovd  44166  fsovcnvlem  44170  dssmapnvod  44177  lhe4.4ex1a  44486  dvradcnv2  44504  binomcxplemdvbinom  44510  binomcxp  44514  fprodcn  45762  limsup0  45854  dvmptfprod  46105  dvnprodlem2  46107  dvnprodlem3  46108  dvnprod  46109  iblsplit  46126  itgiccshift  46140  itgperiod  46141  stoweidlem17  46177  dirkeritg  46262  dirkercncf  46267  fourierdlem60  46326  fourierdlem61  46327  fourierdlem93  46359  fourierdlem100  46366  fourierdlem109  46375  fourierdlem112  46378  etransclem13  46407  etransclem46  46440  subsaliuncl  46518  sge0xaddlem2  46594  meaiuninc  46641  caratheodorylem1  46686  caratheodory  46688  hoicvrrex  46716  ovnsubadd  46732  sge0hsphoire  46749  hoidmv1le  46754  hoidmvlelem1  46755  hoidmvlelem2  46756  hoidmvlelem3  46757  hoidmvlelem4  46758  hoidmvlelem5  46759  hoidmvle  46760  ovnhoi  46763  hspdifhsp  46776  hspmbllem3  46788  hspmbl  46789  iccvonmbl  46839  vonicc  46845  vonn0ioo  46847  vonn0icc  46848  smfadd  46925  smflimlem4  46934  smflimsuplem1  46980  smflimsup  46988  dflinc2  48572