Theorem mpteq2i 5252

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

Syntax hints:   = wceq 1539   ∈ wcel 2104   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-opab 5210  df-mpt 5231

This theorem is referenced by:  offval22  8076  offsplitfpar  8107  konigth  10566  ofccat  14920  rlimneg  15597  cbvprod  15863  eirrlem  16151  lubfval  18307  glbfval  18320  odulub  18364  oduglb  18366  ablfaclem3  19998  znzrh2  21320  mplcoe3  21812  evlsval  21868  gsummoncoe1  22048  matgsum  22159  mat1f1o  22200  scmatscm  22235  mulmarep1gsum1  22295  mdettpos  22333  mp2pm2mplem4  22531  mp2pm2mplem5  22532  mp2pm2mp  22533  cpmidpmat  22595  cnmpt12f  23390  cnmptkc  23403  xkohmeo  23539  qustgpopn  23844  fsumcn  24608  ovolctb  25239  itg2monolem3  25502  dfitg  25519  itg0  25529  iblre  25543  itgreval  25546  iblconst  25567  itgconst  25568  ibladdlem  25569  itgaddlem1  25572  itgfsum  25576  iblabs  25578  itgsplit  25585  dvmptfsum  25727  dvef  25732  dvsincos  25733  dvlipcn  25746  dvfsumge  25774  coemullem  25999  dvtaylp  26118  taylthlem2  26122  pige3ALT  26265  advlogexp  26399  logtayl  26404  loglesqrt  26502  dvatan  26676  basellem2  26822  wlkson  29180  pthsfval  29245  fusgreghash2wsp  29858  rabfmpunirn  32145  zartopn  33153  eulerpart  33679  satf0  34661  neibastop2  35549  ibladdnclem  36847  itgaddnclem1  36849  iblabsnc  36855  iblmulc2nc  36856  ftc1anclem8  36871  dvasin  36875  areacirclem1  36879  lshpkrlem3  38285  lcfrlem39  40755  hdmap1cbv  40976  mzpnegmpt  41784  mzpresrename  41790  areaquad  42267  dfid7  42665  dfrtrcl5  42682  dfrcl4  42729  fsovrfovd  43062  fsovcnvlem  43066  dssmapnvod  43073  lhe4.4ex1a  43390  dvradcnv2  43408  binomcxplemdvbinom  43414  binomcxp  43418  fprodcn  44614  limsup0  44708  dvmptfprod  44959  dvnprodlem2  44961  dvnprodlem3  44962  dvnprod  44963  iblsplit  44980  itgiccshift  44994  itgperiod  44995  stoweidlem17  45031  dirkeritg  45116  dirkercncf  45121  fourierdlem60  45180  fourierdlem61  45181  fourierdlem93  45213  fourierdlem100  45220  fourierdlem109  45229  fourierdlem112  45232  etransclem13  45261  etransclem46  45294  subsaliuncl  45372  sge0xaddlem2  45448  meaiuninc  45495  caratheodorylem1  45540  caratheodory  45542  hoicvrrex  45570  ovnsubadd  45586  sge0hsphoire  45603  hoidmv1le  45608  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem3  45611  hoidmvlelem4  45612  hoidmvlelem5  45613  hoidmvle  45614  ovnhoi  45617  hspdifhsp  45630  hspmbllem3  45642  hspmbl  45643  iccvonmbl  45693  vonicc  45699  vonn0ioo  45701  vonn0icc  45702  smfadd  45779  smflimlem4  45788  smflimsuplem1  45834  smflimsup  45842  dflinc2  47178