Theorem mpteq2i 4741

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpteq2i.1	|- B = C

Assertion

Ref	Expression
mpteq2i	|- ( x e. A |-> B ) = ( x e. A |-> C )

Proof of Theorem mpteq2i

Step	Hyp	Ref	Expression
1		mpteq2i.1	. . 3 |- B = C
2	1	a1i 11	. 2 |- ( x e. A -> B = C )
3	2	mpteq2ia 4740	1 |- ( x e. A |-> B ) = ( x e. A |-> C )

Syntax hints:   = wceq 1483   e. wcel 1990   |-> cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  offval22  7253  konigth  9391  ofccat  13708  rlimneg  14377  cbvprod  14645  eirrlem  14932  ndxidOLD  15884  dfpleOLD  15962  lubfval  16978  glbfval  16991  oduglb  17139  odulub  17141  ablfaclem3  18486  mplcoe3  19466  evlsval  19519  gsummoncoe1  19674  znzrh2  19894  matgsum  20243  mat1f1o  20284  scmatscm  20319  mulmarep1gsum1  20379  mdettpos  20417  mp2pm2mplem4  20614  mp2pm2mplem5  20615  mp2pm2mp  20616  cpmidpmat  20678  cnmpt12f  21469  cnmptkc  21482  xkohmeo  21618  qustgpopn  21923  fsumcn  22673  ovolctb  23258  itg2monolem3  23519  dfitg  23536  itg0  23546  iblre  23560  itgreval  23563  iblconst  23584  itgconst  23585  ibladdlem  23586  itgaddlem1  23589  itgfsum  23593  iblabs  23595  itgsplit  23602  dvmptfsum  23738  dvef  23743  dvsincos  23744  dvlipcn  23757  dvfsumge  23785  coemullem  24006  dvtaylp  24124  taylthlem2  24128  pige3  24269  advlogexp  24401  logtayl  24406  loglesqrt  24499  dvatan  24662  basellem2  24808  wlkson  26552  pthsfval  26617  fusgreghash2wsp  27202  rabfmpunirn  29453  eulerpart  30444  trpredlem1  31727  trpred0  31736  neibastop2  32356  ibladdnclem  33466  itgaddnclem1  33468  iblabsnc  33474  iblmulc2nc  33475  ftc1anclem8  33492  dvasin  33496  areacirclem1  33500  lshpkrlem3  34399  lcfrlem39  36870  hdmap1cbv  37092  mzpnegmpt  37307  mzpresrename  37313  areaquad  37802  dfid7  37919  dfrtrcl5  37936  dfrcl4  37968  fsovrfovd  38303  fsovcnvlem  38307  dssmapnvod  38314  lhe4.4ex1a  38528  dvradcnv2  38546  binomcxplemdvbinom  38552  binomcxp  38556  fprodcn  39832  limsup0  39926  dvmptfprod  40160  dvnprodlem2  40162  dvnprodlem3  40163  dvnprod  40164  iblsplit  40182  itgiccshift  40196  itgperiod  40197  stoweidlem17  40234  dirkeritg  40319  dirkercncf  40324  fourierdlem60  40383  fourierdlem61  40384  fourierdlem93  40416  fourierdlem100  40423  fourierdlem109  40432  fourierdlem112  40435  etransclem13  40464  etransclem46  40497  subsaliuncl  40576  sge0xaddlem2  40651  meaiuninc  40698  caratheodorylem1  40740  caratheodory  40742  hoicvrrex  40770  ovnsubadd  40786  sge0hsphoire  40803  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvlelem5  40813  hoidmvle  40814  ovnhoi  40817  hspdifhsp  40830  hspmbllem3  40842  hspmbl  40843  iccvonmbl  40893  vonicc  40899  vonn0ioo  40901  vonn0icc  40902  smfadd  40973  smflimlem4  40982  smflimsuplem1  41026  smflimsup  41034  dflinc2  42199