Theorem mpteq2i 5201

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-mpt 5187

This theorem is used by:  offval22  8085  offsplitfpar  8116  konigth  10578  ofccat  15042  rlimneg  15734  cbvsumv  15783  cbvprod  16002  cbvprodv  16003  prodeq1i  16005  eirrlem  16292  lubfval  18436  glbfval  18449  odulub  18493  oduglb  18495  ablfaclem3  20216  znzrh2  21758  mplcoe3  22254  evlsval  22302  psdmul  22394  gsummoncoe1  22533  matgsum  22659  mat1f1o  22700  scmatscm  22735  mulmarep1gsum1  22795  mdettpos  22833  mp2pm2mplem4  23034  mp2pm2mplem5  23035  mp2pm2mp  23036  cpmidpmat  23098  cnmpt12f  23892  cnmptkc  23905  xkohmeo  24041  qustgpopn  24346  fsumcn  25098  ovolctb  25718  itg2monolem3  25980  dfitg  25997  itg0  26007  iblre  26021  itgreval  26024  iblconst  26045  itgconst  26046  ibladdlem  26047  itgaddlem1  26050  itgfsum  26054  iblabs  26056  itgsplit  26063  dvmptfsum  26202  dvef  26207  dvsincos  26208  dvlipcn  26221  dvfsumge  26249  coemullem  26476  dvtaylp  26606  taylthlem2  26610  pige3ALT  26757  advlogexp  26892  logtayl  26897  loglesqrt  26998  dvatan  27172  basellem2  27318  wlkson  30114  pthsfval  30183  fusgreghash2wsp  30818  rabfmpunirn  33126  selvply1rhmlem5  34034  selvply1rhm  34035  mplidom  34038  psrmonprod  34062  constrcbvlem  34265  zartopn  34385  eulerpart  34893  fineqvnttrclse  35650  satf0  35951  sumeq2si  36822  prodeq2si  36824  itgeq12i  36826  cbvprodvw2  36867  neibastop2  36980  ibladdnclem  38425  itgaddnclem1  38427  iblabsnc  38433  iblmulc2nc  38434  ftc1anclem8  38449  dvasin  38453  areacirclem1  38457  dfqmap2  39195  lshpkrlem3  39985  lcfrlem39  42454  hdmap1cbv  42675  redvmptabs  43235  mzpnegmpt  43589  mzpresrename  43595  areaquad  44057  dfid7  44452  dfrtrcl5  44469  dfrcl4  44516  fsovrfovd  44849  fsovcnvlem  44853  dssmapnvod  44860  lhe4.4ex1a  45153  dvradcnv2  45171  binomcxplemdvbinom  45177  binomcxp  45181  fprodcn  46430  limsup0  46522  dvmptfprod  46773  dvnprodlem2  46775  dvnprodlem3  46776  dvnprod  46777  iblsplit  46794  itgiccshift  46808  itgperiod  46809  stoweidlem17  46845  dirkeritg  46930  dirkercncf  46935  fourierdlem60  46994  fourierdlem61  46995  fourierdlem93  47027  fourierdlem100  47034  fourierdlem109  47043  fourierdlem112  47046  etransclem13  47075  etransclem46  47108  subsaliuncl  47186  sge0xaddlem2  47262  meaiuninc  47309  caratheodorylem1  47354  caratheodory  47356  hoicvrrex  47384  ovnsubadd  47400  sge0hsphoire  47417  hoidmv1le  47422  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvlelem4  47426  hoidmvlelem5  47427  hoidmvle  47428  ovnhoi  47431  hspdifhsp  47444  hspmbllem3  47456  hspmbl  47457  iccvonmbl  47507  vonicc  47513  vonn0ioo  47515  vonn0icc  47516  smfadd  47593  smflimlem4  47602  smflimsuplem1  47648  smflimsup  47656  dflinc2  49340  veroquadmodzerod  50817