Theorem mpteq2i 5184

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

Syntax hints:   = wceq 1542   ∈ wcel 2110   ↦ cmpt 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-opab 5142  df-mpt 5163

This theorem is referenced by:  offval22  7919  offsplitfpar  7951  trpredlem1  9474  trpred0  9479  konigth  10326  ofccat  14678  rlimneg  15356  cbvprod  15623  eirrlem  15911  lubfval  18066  glbfval  18079  odulub  18123  oduglb  18125  ablfaclem3  19688  znzrh2  20751  mplcoe3  21237  evlsval  21294  gsummoncoe1  21473  matgsum  21584  mat1f1o  21625  scmatscm  21660  mulmarep1gsum1  21720  mdettpos  21758  mp2pm2mplem4  21956  mp2pm2mplem5  21957  mp2pm2mp  21958  cpmidpmat  22020  cnmpt12f  22815  cnmptkc  22828  xkohmeo  22964  qustgpopn  23269  fsumcn  24031  ovolctb  24652  itg2monolem3  24915  dfitg  24932  itg0  24942  iblre  24956  itgreval  24959  iblconst  24980  itgconst  24981  ibladdlem  24982  itgaddlem1  24985  itgfsum  24989  iblabs  24991  itgsplit  24998  dvmptfsum  25137  dvef  25142  dvsincos  25143  dvlipcn  25156  dvfsumge  25184  coemullem  25409  dvtaylp  25527  taylthlem2  25531  pige3ALT  25674  advlogexp  25808  logtayl  25813  loglesqrt  25909  dvatan  26083  basellem2  26229  wlkson  28021  pthsfval  28085  fusgreghash2wsp  28698  rabfmpunirn  30986  zartopn  31821  eulerpart  32345  satf0  33330  neibastop2  34546  ibladdnclem  35829  itgaddnclem1  35831  iblabsnc  35837  iblmulc2nc  35838  ftc1anclem8  35853  dvasin  35857  areacirclem1  35861  lshpkrlem3  37122  lcfrlem39  39591  hdmap1cbv  39812  mzpnegmpt  40563  mzpresrename  40569  areaquad  41044  dfid7  41190  dfrtrcl5  41207  dfrcl4  41254  fsovrfovd  41587  fsovcnvlem  41591  dssmapnvod  41598  lhe4.4ex1a  41917  dvradcnv2  41935  binomcxplemdvbinom  41941  binomcxp  41945  fprodcn  43112  limsup0  43206  dvmptfprod  43457  dvnprodlem2  43459  dvnprodlem3  43460  dvnprod  43461  iblsplit  43478  itgiccshift  43492  itgperiod  43493  stoweidlem17  43529  dirkeritg  43614  dirkercncf  43619  fourierdlem60  43678  fourierdlem61  43679  fourierdlem93  43711  fourierdlem100  43718  fourierdlem109  43727  fourierdlem112  43730  etransclem13  43759  etransclem46  43792  subsaliuncl  43868  sge0xaddlem2  43943  meaiuninc  43990  caratheodorylem1  44035  caratheodory  44037  hoicvrrex  44065  ovnsubadd  44081  sge0hsphoire  44098  hoidmv1le  44103  hoidmvlelem1  44104  hoidmvlelem2  44105  hoidmvlelem3  44106  hoidmvlelem4  44107  hoidmvlelem5  44108  hoidmvle  44109  ovnhoi  44112  hspdifhsp  44125  hspmbllem3  44137  hspmbl  44138  iccvonmbl  44188  vonicc  44194  vonn0ioo  44196  vonn0icc  44197  smfadd  44268  smflimlem4  44277  smflimsuplem1  44321  smflimsup  44329  dflinc2  45720