Theorem mpteq2i 5179

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

Syntax hints:   = wceq 1539   ∈ wcel 2106   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-mpt 5158

This theorem is referenced by:  offval22  7928  offsplitfpar  7960  konigth  10325  ofccat  14680  rlimneg  15358  cbvprod  15625  eirrlem  15913  lubfval  18068  glbfval  18081  odulub  18125  oduglb  18127  ablfaclem3  19690  znzrh2  20753  mplcoe3  21239  evlsval  21296  gsummoncoe1  21475  matgsum  21586  mat1f1o  21627  scmatscm  21662  mulmarep1gsum1  21722  mdettpos  21760  mp2pm2mplem4  21958  mp2pm2mplem5  21959  mp2pm2mp  21960  cpmidpmat  22022  cnmpt12f  22817  cnmptkc  22830  xkohmeo  22966  qustgpopn  23271  fsumcn  24033  ovolctb  24654  itg2monolem3  24917  dfitg  24934  itg0  24944  iblre  24958  itgreval  24961  iblconst  24982  itgconst  24983  ibladdlem  24984  itgaddlem1  24987  itgfsum  24991  iblabs  24993  itgsplit  25000  dvmptfsum  25139  dvef  25144  dvsincos  25145  dvlipcn  25158  dvfsumge  25186  coemullem  25411  dvtaylp  25529  taylthlem2  25533  pige3ALT  25676  advlogexp  25810  logtayl  25815  loglesqrt  25911  dvatan  26085  basellem2  26231  wlkson  28024  pthsfval  28089  fusgreghash2wsp  28702  rabfmpunirn  30990  zartopn  31825  eulerpart  32349  satf0  33334  neibastop2  34550  ibladdnclem  35833  itgaddnclem1  35835  iblabsnc  35841  iblmulc2nc  35842  ftc1anclem8  35857  dvasin  35861  areacirclem1  35865  lshpkrlem3  37126  lcfrlem39  39595  hdmap1cbv  39816  mzpnegmpt  40566  mzpresrename  40572  areaquad  41047  dfid7  41220  dfrtrcl5  41237  dfrcl4  41284  fsovrfovd  41617  fsovcnvlem  41621  dssmapnvod  41628  lhe4.4ex1a  41947  dvradcnv2  41965  binomcxplemdvbinom  41971  binomcxp  41975  fprodcn  43141  limsup0  43235  dvmptfprod  43486  dvnprodlem2  43488  dvnprodlem3  43489  dvnprod  43490  iblsplit  43507  itgiccshift  43521  itgperiod  43522  stoweidlem17  43558  dirkeritg  43643  dirkercncf  43648  fourierdlem60  43707  fourierdlem61  43708  fourierdlem93  43740  fourierdlem100  43747  fourierdlem109  43756  fourierdlem112  43759  etransclem13  43788  etransclem46  43821  subsaliuncl  43897  sge0xaddlem2  43972  meaiuninc  44019  caratheodorylem1  44064  caratheodory  44066  hoicvrrex  44094  ovnsubadd  44110  sge0hsphoire  44127  hoidmv1le  44132  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvlelem4  44136  hoidmvlelem5  44137  hoidmvle  44138  ovnhoi  44141  hspdifhsp  44154  hspmbllem3  44166  hspmbl  44167  iccvonmbl  44217  vonicc  44223  vonn0ioo  44225  vonn0icc  44226  smfadd  44300  smflimlem4  44309  smflimsuplem1  44353  smflimsup  44361  dflinc2  45751