Theorem mpteq2i 5200

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  offval22  8100  offsplitfpar  8133  konigth  10658  ofccat  15128  rlimneg  15820  cbvsumv  15869  cbvprod  16088  cbvprodv  16089  prodeq1i  16091  eirrlem  16378  lubfval  18528  glbfval  18541  odulub  18585  oduglb  18587  ablfaclem3  20309  znzrh2  21857  mplcoe3  22353  evlsval  22401  psdmul  22493  gsummoncoe1  22632  matgsum  22758  mat1f1o  22799  scmatscm  22834  mulmarep1gsum1  22894  mdettpos  22932  mp2pm2mplem4  23133  mp2pm2mplem5  23134  mp2pm2mp  23135  cpmidpmat  23197  cnmpt12f  23991  cnmptkc  24004  xkohmeo  24140  qustgpopn  24445  fsumcn  25197  ovolctb  25817  itg2monolem3  26079  dfitg  26096  itg0  26106  iblre  26120  itgreval  26123  iblconst  26144  itgconst  26145  ibladdlem  26146  itgaddlem1  26149  itgfsum  26153  iblabs  26155  itgsplit  26162  dvmptfsum  26301  dvef  26306  dvsincos  26307  dvlipcn  26320  dvfsumge  26348  coemullem  26575  dvtaylp  26703  taylthlem2  26707  pige3ALT  26854  advlogexp  26989  logtayl  26994  loglesqrt  27095  dvatan  27269  basellem2  27415  wlkson  30241  pthsfval  30310  fusgreghash2wsp  30945  rabfmpunirn  33295  selvply1rhmlem5  34203  selvply1rhm  34204  mplidom  34207  psrmonprod  34231  constrcbvlem  34434  zartopn  34554  eulerpart  35061  fineqvnttrclse  35849  satf0  36224  sumeq2si  37084  prodeq2si  37086  itgeq12i  37088  cbvprodvw2  37129  neibastop2  37242  ibladdnclem  38688  itgaddnclem1  38690  iblabsnc  38696  iblmulc2nc  38697  ftc1anclem8  38712  dvasin  38716  areacirclem1  38720  dfqmap2  39473  lshpkrlem3  40263  lcfrlem39  42732  hdmap1cbv  42953  redvmptabs  43505  mzpnegmpt  43849  mzpresrename  43855  areaquad  44312  dfid7  44706  dfrtrcl5  44723  dfrcl4  44770  fsovrfovd  45103  fsovcnvlem  45107  dssmapnvod  45114  lhe4.4ex1a  45407  dvradcnv2  45425  binomcxplemdvbinom  45431  binomcxp  45435  fprodcn  46706  limsup0  46798  dvmptfprod  47049  dvnprodlem2  47051  dvnprodlem3  47052  dvnprod  47053  iblsplit  47070  itgiccshift  47084  itgperiod  47085  stoweidlem17  47121  dirkeritg  47206  dirkercncf  47211  fourierdlem60  47270  fourierdlem61  47271  fourierdlem93  47303  fourierdlem100  47310  fourierdlem109  47319  fourierdlem112  47322  etransclem13  47351  etransclem46  47384  subsaliuncl  47462  sge0xaddlem2  47538  meaiuninc  47585  caratheodorylem1  47630  caratheodory  47632  hoicvrrex  47660  ovnsubadd  47676  sge0hsphoire  47693  hoidmv1le  47698  hoidmvlelem1  47699  hoidmvlelem2  47700  hoidmvlelem3  47701  hoidmvlelem4  47702  hoidmvlelem5  47703  hoidmvle  47704  ovnhoi  47707  hspdifhsp  47720  hspmbllem3  47732  hspmbl  47733  iccvonmbl  47783  vonicc  47789  vonn0ioo  47791  vonn0icc  47792  smfadd  47869  smflimlem4  47878  smflimsuplem1  47924  smflimsup  47932  dflinc2  49616  veroquadmodzerod  51153