Theorem mpteq2i 4976

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

Syntax hints:   = wceq 1601   ∈ wcel 2107   ↦ cmpt 4965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-ral 3095  df-opab 4949  df-mpt 4966

This theorem is referenced by:  offval22  7534  konigth  9726  ofccat  14117  rlimneg  14785  cbvprod  15048  eirrlem  15336  lubfval  17364  glbfval  17377  oduglb  17525  odulub  17527  ablfaclem3  18873  mplcoe3  19863  evlsval  19915  gsummoncoe1  20070  znzrh2  20289  matgsum  20647  mat1f1o  20689  scmatscm  20724  mulmarep1gsum1  20784  mdettpos  20822  mp2pm2mplem4  21021  mp2pm2mplem5  21022  mp2pm2mp  21023  cpmidpmat  21085  cnmpt12f  21878  cnmptkc  21891  xkohmeo  22027  qustgpopn  22331  fsumcn  23081  ovolctb  23694  itg2monolem3  23956  dfitg  23973  itg0  23983  iblre  23997  itgreval  24000  iblconst  24021  itgconst  24022  ibladdlem  24023  itgaddlem1  24026  itgfsum  24030  iblabs  24032  itgsplit  24039  dvmptfsum  24175  dvef  24180  dvsincos  24181  dvlipcn  24194  dvfsumge  24222  coemullem  24443  dvtaylp  24561  taylthlem2  24565  pige3  24707  advlogexp  24838  logtayl  24843  loglesqrt  24939  dvatan  25113  basellem2  25260  wlkson  27003  pthsfval  27073  fusgreghash2wsp  27746  rabfmpunirn  30018  eulerpart  31042  trpredlem1  32315  trpred0  32324  neibastop2  32944  ibladdnclem  34093  itgaddnclem1  34095  iblabsnc  34101  iblmulc2nc  34102  ftc1anclem8  34119  dvasin  34123  areacirclem1  34127  lshpkrlem3  35268  lcfrlem39  37737  hdmap1cbv  37958  mzpnegmpt  38271  mzpresrename  38277  areaquad  38764  dfid7  38880  dfrtrcl5  38897  dfrcl4  38929  fsovrfovd  39263  fsovcnvlem  39267  dssmapnvod  39274  lhe4.4ex1a  39488  dvradcnv2  39506  binomcxplemdvbinom  39512  binomcxp  39516  fprodcn  40744  limsup0  40838  dvmptfprod  41092  dvnprodlem2  41094  dvnprodlem3  41095  dvnprod  41096  iblsplit  41113  itgiccshift  41127  itgperiod  41128  stoweidlem17  41165  dirkeritg  41250  dirkercncf  41255  fourierdlem60  41314  fourierdlem61  41315  fourierdlem93  41347  fourierdlem100  41354  fourierdlem109  41363  fourierdlem112  41366  etransclem13  41395  etransclem46  41428  subsaliuncl  41504  sge0xaddlem2  41579  meaiuninc  41626  caratheodorylem1  41671  caratheodory  41673  hoicvrrex  41701  ovnsubadd  41717  sge0hsphoire  41734  hoidmv1le  41739  hoidmvlelem1  41740  hoidmvlelem2  41741  hoidmvlelem3  41742  hoidmvlelem4  41743  hoidmvlelem5  41744  hoidmvle  41745  ovnhoi  41748  hspdifhsp  41761  hspmbllem3  41773  hspmbl  41774  iccvonmbl  41824  vonicc  41830  vonn0ioo  41832  vonn0icc  41833  smfadd  41904  smflimlem4  41913  smflimsuplem1  41957  smflimsup  41965  dflinc2  43218