Theorem mpteq2i 5205

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147   ↦ cmpt 5190

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-mpt 5191

This theorem is used by:  offval22  8132  offsplitfpar  8165  konigth  10691  ofccat  15163  rlimneg  15855  cbvsumv  15904  cbvprod  16123  cbvprodv  16124  prodeq1i  16126  eirrlem  16413  lubfval  18563  glbfval  18576  odulub  18620  oduglb  18622  ablfaclem3  20345  znzrh2  21895  mplcoe3  22391  evlsval  22439  psdmul  22531  gsummoncoe1  22670  matgsum  22796  mat1f1o  22837  scmatscm  22872  mulmarep1gsum1  22932  mdettpos  22970  mp2pm2mplem4  23171  mp2pm2mplem5  23172  mp2pm2mp  23173  cpmidpmat  23235  cnmpt12f  24029  cnmptkc  24042  xkohmeo  24178  qustgpopn  24483  fsumcn  25235  ovolctb  25855  itg2monolem3  26117  dfitg  26134  itg0  26144  iblre  26158  itgreval  26161  iblconst  26182  itgconst  26183  ibladdlem  26184  itgaddlem1  26187  itgfsum  26191  iblabs  26193  itgsplit  26200  dvmptfsum  26339  dvef  26344  dvsincos  26345  dvlipcn  26358  dvfsumge  26386  coemullem  26613  dvtaylp  26743  taylthlem2  26747  pige3ALT  26894  advlogexp  27029  logtayl  27034  loglesqrt  27135  dvatan  27309  basellem2  27455  wlkson  30281  pthsfval  30350  fusgreghash2wsp  30985  rabfmpunirn  33335  selvply1rhmlem5  34260  selvply1rhm  34261  mplidom  34264  psrmonprod  34288  constrcbvlem  34491  zartopn  34611  eulerpart  35118  fineqvnttrclse  35926  satf0  36338  sumeq2si  37199  prodeq2si  37201  itgeq12i  37203  cbvprodvw2  37244  neibastop2  37357  ibladdnclem  38855  itgaddnclem1  38857  iblabsnc  38863  iblmulc2nc  38864  ftc1anclem8  38879  dvasin  38883  areacirclem1  38887  dfqmap2  39638  lshpkrlem3  40428  lcfrlem39  42897  hdmap1cbv  43118  redvmptabs  43671  mzpnegmpt  44015  mzpresrename  44021  areaquad  44473  dfid7  44867  dfrtrcl5  44884  dfrcl4  44931  fsovrfovd  45264  fsovcnvlem  45268  dssmapnvod  45275  lhe4.4ex1a  45568  dvradcnv2  45586  binomcxplemdvbinom  45592  binomcxp  45596  ackbij3  46283  fprodcn  46879  limsup0  46971  dvmptfprod  47222  dvnprodlem2  47224  dvnprodlem3  47225  dvnprod  47226  iblsplit  47243  itgiccshift  47257  itgperiod  47258  stoweidlem17  47294  dirkeritg  47379  dirkercncf  47384  fourierdlem60  47443  fourierdlem61  47444  fourierdlem93  47476  fourierdlem100  47483  fourierdlem109  47492  fourierdlem112  47495  etransclem13  47524  etransclem46  47557  subsaliuncl  47635  sge0xaddlem2  47711  meaiuninc  47758  caratheodorylem1  47803  caratheodory  47805  hoicvrrex  47833  ovnsubadd  47849  sge0hsphoire  47866  hoidmv1le  47871  hoidmvlelem1  47872  hoidmvlelem2  47873  hoidmvlelem3  47874  hoidmvlelem4  47875  hoidmvlelem5  47876  hoidmvle  47877  ovnhoi  47880  hspdifhsp  47893  hspmbllem3  47905  hspmbl  47906  iccvonmbl  47956  vonicc  47962  vonn0ioo  47964  vonn0icc  47965  smfadd  48042  smflimlem4  48051  smflimsuplem1  48097  smflimsup  48105  dflinc2  49847  veroquadmodzerod  51406