Theorem mpteq2i 5160

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

Syntax hints:   = wceq 1537   ∈ wcel 2114   ↦ cmpt 5148

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-opab 5131  df-mpt 5149

This theorem is referenced by:  offval22  7785  offsplitfpar  7817  konigth  9993  ofccat  14331  rlimneg  15005  cbvprod  15271  eirrlem  15559  lubfval  17590  glbfval  17603  oduglb  17751  odulub  17753  ablfaclem3  19211  mplcoe3  20249  evlsval  20301  gsummoncoe1  20474  znzrh2  20694  matgsum  21048  mat1f1o  21089  scmatscm  21124  mulmarep1gsum1  21184  mdettpos  21222  mp2pm2mplem4  21419  mp2pm2mplem5  21420  mp2pm2mp  21421  cpmidpmat  21483  cnmpt12f  22276  cnmptkc  22289  xkohmeo  22425  qustgpopn  22730  fsumcn  23480  ovolctb  24093  itg2monolem3  24355  dfitg  24372  itg0  24382  iblre  24396  itgreval  24399  iblconst  24420  itgconst  24421  ibladdlem  24422  itgaddlem1  24425  itgfsum  24429  iblabs  24431  itgsplit  24438  dvmptfsum  24574  dvef  24579  dvsincos  24580  dvlipcn  24593  dvfsumge  24621  coemullem  24842  dvtaylp  24960  taylthlem2  24964  pige3ALT  25107  advlogexp  25240  logtayl  25245  loglesqrt  25341  dvatan  25515  basellem2  25661  wlkson  27440  pthsfval  27504  fusgreghash2wsp  28119  rabfmpunirn  30400  eulerpart  31642  satf0  32621  trpredlem1  33068  trpred0  33077  neibastop2  33711  ibladdnclem  34950  itgaddnclem1  34952  iblabsnc  34958  iblmulc2nc  34959  ftc1anclem8  34976  dvasin  34980  areacirclem1  34984  lshpkrlem3  36250  lcfrlem39  38719  hdmap1cbv  38940  mzpnegmpt  39348  mzpresrename  39354  areaquad  39830  dfid7  39979  dfrtrcl5  39996  dfrcl4  40028  fsovrfovd  40362  fsovcnvlem  40366  dssmapnvod  40373  lhe4.4ex1a  40668  dvradcnv2  40686  binomcxplemdvbinom  40692  binomcxp  40696  fprodcn  41888  limsup0  41982  dvmptfprod  42237  dvnprodlem2  42239  dvnprodlem3  42240  dvnprod  42241  iblsplit  42258  itgiccshift  42272  itgperiod  42273  stoweidlem17  42309  dirkeritg  42394  dirkercncf  42399  fourierdlem60  42458  fourierdlem61  42459  fourierdlem93  42491  fourierdlem100  42498  fourierdlem109  42507  fourierdlem112  42510  etransclem13  42539  etransclem46  42572  subsaliuncl  42648  sge0xaddlem2  42723  meaiuninc  42770  caratheodorylem1  42815  caratheodory  42817  hoicvrrex  42845  ovnsubadd  42861  sge0hsphoire  42878  hoidmv1le  42883  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvlelem4  42887  hoidmvlelem5  42888  hoidmvle  42889  ovnhoi  42892  hspdifhsp  42905  hspmbllem3  42917  hspmbl  42918  iccvonmbl  42968  vonicc  42974  vonn0ioo  42976  vonn0icc  42977  smfadd  43048  smflimlem4  43057  smflimsuplem1  43101  smflimsup  43109  dflinc2  44472