Theorem mpteq2i 5175

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

Syntax hints:   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-mpt 5154

This theorem is referenced by:  offval22  7899  offsplitfpar  7931  trpredlem1  9405  trpred0  9410  konigth  10256  ofccat  14608  rlimneg  15286  cbvprod  15553  eirrlem  15841  lubfval  17983  glbfval  17996  odulub  18040  oduglb  18042  ablfaclem3  19605  znzrh2  20665  mplcoe3  21149  evlsval  21206  gsummoncoe1  21385  matgsum  21494  mat1f1o  21535  scmatscm  21570  mulmarep1gsum1  21630  mdettpos  21668  mp2pm2mplem4  21866  mp2pm2mplem5  21867  mp2pm2mp  21868  cpmidpmat  21930  cnmpt12f  22725  cnmptkc  22738  xkohmeo  22874  qustgpopn  23179  fsumcn  23939  ovolctb  24559  itg2monolem3  24822  dfitg  24839  itg0  24849  iblre  24863  itgreval  24866  iblconst  24887  itgconst  24888  ibladdlem  24889  itgaddlem1  24892  itgfsum  24896  iblabs  24898  itgsplit  24905  dvmptfsum  25044  dvef  25049  dvsincos  25050  dvlipcn  25063  dvfsumge  25091  coemullem  25316  dvtaylp  25434  taylthlem2  25438  pige3ALT  25581  advlogexp  25715  logtayl  25720  loglesqrt  25816  dvatan  25990  basellem2  26136  wlkson  27926  pthsfval  27990  fusgreghash2wsp  28603  rabfmpunirn  30892  zartopn  31727  eulerpart  32249  satf0  33234  neibastop2  34477  ibladdnclem  35760  itgaddnclem1  35762  iblabsnc  35768  iblmulc2nc  35769  ftc1anclem8  35784  dvasin  35788  areacirclem1  35792  lshpkrlem3  37053  lcfrlem39  39522  hdmap1cbv  39743  mzpnegmpt  40482  mzpresrename  40488  areaquad  40963  dfid7  41109  dfrtrcl5  41126  dfrcl4  41173  fsovrfovd  41506  fsovcnvlem  41510  dssmapnvod  41517  lhe4.4ex1a  41836  dvradcnv2  41854  binomcxplemdvbinom  41860  binomcxp  41864  fprodcn  43031  limsup0  43125  dvmptfprod  43376  dvnprodlem2  43378  dvnprodlem3  43379  dvnprod  43380  iblsplit  43397  itgiccshift  43411  itgperiod  43412  stoweidlem17  43448  dirkeritg  43533  dirkercncf  43538  fourierdlem60  43597  fourierdlem61  43598  fourierdlem93  43630  fourierdlem100  43637  fourierdlem109  43646  fourierdlem112  43649  etransclem13  43678  etransclem46  43711  subsaliuncl  43787  sge0xaddlem2  43862  meaiuninc  43909  caratheodorylem1  43954  caratheodory  43956  hoicvrrex  43984  ovnsubadd  44000  sge0hsphoire  44017  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidmvle  44028  ovnhoi  44031  hspdifhsp  44044  hspmbllem3  44056  hspmbl  44057  iccvonmbl  44107  vonicc  44113  vonn0ioo  44115  vonn0icc  44116  smfadd  44187  smflimlem4  44196  smflimsuplem1  44240  smflimsup  44248  dflinc2  45639