Theorem mpteq2i 5168

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

Syntax hints:   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5153

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-mpt 5154

This theorem is referenced by:  offval22  8027  offsplitfpar  8058  konigth  10483  ofccat  14922  rlimneg  15600  cbvsumv  15649  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  eirrlem  16162  lubfval  18305  glbfval  18318  odulub  18362  oduglb  18364  ablfaclem3  20055  znzrh2  21520  mplcoe3  22014  evlsval  22062  psdmul  22154  gsummoncoe1  22294  matgsum  22420  mat1f1o  22461  scmatscm  22496  mulmarep1gsum1  22556  mdettpos  22594  mp2pm2mplem4  22792  mp2pm2mplem5  22793  mp2pm2mp  22794  cpmidpmat  22856  cnmpt12f  23649  cnmptkc  23662  xkohmeo  23798  qustgpopn  24103  fsumcn  24855  ovolctb  25475  itg2monolem3  25737  dfitg  25754  itg0  25765  iblre  25779  itgreval  25782  iblconst  25803  itgconst  25804  ibladdlem  25805  itgaddlem1  25808  itgfsum  25812  iblabs  25814  itgsplit  25821  dvmptfsum  25960  dvef  25965  dvsincos  25966  dvlipcn  25979  dvfsumge  26007  coemullem  26233  dvtaylp  26353  taylthlem2  26357  pige3ALT  26502  advlogexp  26637  logtayl  26642  loglesqrt  26743  dvatan  26917  basellem2  27063  wlkson  29741  pthsfval  29805  fusgreghash2wsp  30426  rabfmpunirn  32745  selvply1rhmlem5  33708  selvply1rhm  33709  mplidom  33712  psrmonprod  33736  constrcbvlem  33939  zartopn  34059  eulerpart  34566  fineqvnttrclse  35305  satf0  35600  sumeq2si  36430  prodeq2si  36432  itgeq12i  36434  cbvprodvw2  36475  neibastop2  36589  ibladdnclem  38043  itgaddnclem1  38045  iblabsnc  38051  iblmulc2nc  38052  ftc1anclem8  38067  dvasin  38071  areacirclem1  38075  dfqmap2  38814  lshpkrlem3  39604  lcfrlem39  42073  hdmap1cbv  42294  redvmptabs  42837  mzpnegmpt  43193  mzpresrename  43199  areaquad  43661  dfid7  44056  dfrtrcl5  44073  dfrcl4  44120  fsovrfovd  44453  fsovcnvlem  44457  dssmapnvod  44464  lhe4.4ex1a  44773  dvradcnv2  44791  binomcxplemdvbinom  44797  binomcxp  44801  fprodcn  46045  limsup0  46137  dvmptfprod  46388  dvnprodlem2  46390  dvnprodlem3  46391  dvnprod  46392  iblsplit  46409  itgiccshift  46423  itgperiod  46424  stoweidlem17  46460  dirkeritg  46545  dirkercncf  46550  fourierdlem60  46609  fourierdlem61  46610  fourierdlem93  46642  fourierdlem100  46649  fourierdlem109  46658  fourierdlem112  46661  etransclem13  46690  etransclem46  46723  subsaliuncl  46801  sge0xaddlem2  46877  meaiuninc  46924  caratheodorylem1  46969  caratheodory  46971  hoicvrrex  46999  ovnsubadd  47015  sge0hsphoire  47032  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvlelem5  47042  hoidmvle  47043  ovnhoi  47046  hspdifhsp  47059  hspmbllem3  47071  hspmbl  47072  iccvonmbl  47122  vonicc  47128  vonn0ioo  47130  vonn0icc  47131  smfadd  47208  smflimlem4  47217  smflimsuplem1  47263  smflimsup  47271  dflinc2  48901