Theorem mpteq2i 5258

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

Syntax hints:   = wceq 1534   ∈ wcel 2099   ↦ cmpt 5236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-opab 5216  df-mpt 5237

This theorem is referenced by:  offval22  8102  offsplitfpar  8133  konigth  10612  ofccat  14974  rlimneg  15651  cbvprod  15917  eirrlem  16206  lubfval  18375  glbfval  18388  odulub  18432  oduglb  18434  ablfaclem3  20087  znzrh2  21543  mplcoe3  22045  evlsval  22101  psdmul  22160  gsummoncoe1  22299  matgsum  22430  mat1f1o  22471  scmatscm  22506  mulmarep1gsum1  22566  mdettpos  22604  mp2pm2mplem4  22802  mp2pm2mplem5  22803  mp2pm2mp  22804  cpmidpmat  22866  cnmpt12f  23661  cnmptkc  23674  xkohmeo  23810  qustgpopn  24115  fsumcn  24879  ovolctb  25510  itg2monolem3  25773  dfitg  25790  itg0  25800  iblre  25814  itgreval  25817  iblconst  25838  itgconst  25839  ibladdlem  25840  itgaddlem1  25843  itgfsum  25847  iblabs  25849  itgsplit  25856  dvmptfsum  25998  dvef  26003  dvsincos  26004  dvlipcn  26018  dvfsumge  26047  coemullem  26277  dvtaylp  26398  taylthlem2  26402  taylthlem2OLD  26403  pige3ALT  26547  advlogexp  26682  logtayl  26687  loglesqrt  26789  dvatan  26963  basellem2  27110  wlkson  29593  pthsfval  29658  fusgreghash2wsp  30271  rabfmpunirn  32570  zartopn  33690  eulerpart  34216  satf0  35200  neibastop2  36073  ibladdnclem  37377  itgaddnclem1  37379  iblabsnc  37385  iblmulc2nc  37386  ftc1anclem8  37401  dvasin  37405  areacirclem1  37409  lshpkrlem3  38810  lcfrlem39  41280  hdmap1cbv  41501  mzpnegmpt  42401  mzpresrename  42407  areaquad  42881  dfid7  43279  dfrtrcl5  43296  dfrcl4  43343  fsovrfovd  43676  fsovcnvlem  43680  dssmapnvod  43687  lhe4.4ex1a  44003  dvradcnv2  44021  binomcxplemdvbinom  44027  binomcxp  44031  fprodcn  45221  limsup0  45315  dvmptfprod  45566  dvnprodlem2  45568  dvnprodlem3  45569  dvnprod  45570  iblsplit  45587  itgiccshift  45601  itgperiod  45602  stoweidlem17  45638  dirkeritg  45723  dirkercncf  45728  fourierdlem60  45787  fourierdlem61  45788  fourierdlem93  45820  fourierdlem100  45827  fourierdlem109  45836  fourierdlem112  45839  etransclem13  45868  etransclem46  45901  subsaliuncl  45979  sge0xaddlem2  46055  meaiuninc  46102  caratheodorylem1  46147  caratheodory  46149  hoicvrrex  46177  ovnsubadd  46193  sge0hsphoire  46210  hoidmv1le  46215  hoidmvlelem1  46216  hoidmvlelem2  46217  hoidmvlelem3  46218  hoidmvlelem4  46219  hoidmvlelem5  46220  hoidmvle  46221  ovnhoi  46224  hspdifhsp  46237  hspmbllem3  46249  hspmbl  46250  iccvonmbl  46300  vonicc  46306  vonn0ioo  46308  vonn0icc  46309  smfadd  46386  smflimlem4  46395  smflimsuplem1  46441  smflimsup  46449  dflinc2  47793