MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq2dv Unicode version

Theorem mpteq2dv 4238
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
Hypothesis
Ref Expression
mpteq2dv.1  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
mpteq2dv  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)

Proof of Theorem mpteq2dv
StepHypRef Expression
1 mpteq2dv.1 . . 3  |-  ( ph  ->  B  =  C )
21adantr 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
32mpteq2dva 4237 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717    e. cmpt 4208
This theorem is referenced by:  ofeq  6247  rdgeq1  6606  rdgeq2  6607  omv  6693  oev  6695  oieq1  7415  oieq2  7416  cantnflem1  7579  wunex2  8547  wuncval2  8556  reexALT  10539  seqof2  11309  limsupval  12196  sumeq2w  12414  cbvsum  12417  summo  12439  fsum  12442  fsumrlim  12518  fsumo1  12519  rpnnen2lem1  12742  rpnnen2lem2  12743  rpnnen  12754  1arithlem1  13219  vdwapval  13269  vdwlem6  13282  vdwlem8  13284  vdwlem9  13285  vdwlem10  13286  ramub1lem2  13323  ramcl  13325  prdsplusgval  13623  prdsmulrval  13625  prdsdsval  13628  prdsvscaval  13629  ismon  13887  fucco  14087  curf1  14250  curf2  14254  yonedalem4a  14300  grplactfval  14813  galactghm  15034  sylow1  15165  sylow2b  15185  sylow3lem5  15193  sylow3  15195  iscyg  15417  gsumzaddlem  15454  gsumzmhm  15461  ablfac2  15575  gsumdixp  15643  psrmulfval  16377  mvrval  16413  subrgmvr  16452  mplcoe1  16456  mplcoe3  16457  mplcoe2  16458  mplmon2  16481  subrgascl  16486  evlslem2  16496  coe1fval  16531  zncyg  16753  phllmhm  16787  isphld  16809  ptbasfi  17535  ptcnplem  17575  ptrescn  17593  cnmpt2k  17642  xkohmeo  17769  fmval  17897  fmf  17899  ptcmpg  18010  tmdmulg  18044  prdstmdd  18075  tsmspropd  18083  prdsxmslem2  18450  metdsval  18749  fsumcn  18772  expcn  18774  lebnumlem3  18860  pcoval  18908  pi1xfrcnv  18954  itg11  19451  mbfi1fseqlem2  19476  mbfi1fseqlem6  19480  mbfi1fseq  19481  mbfi1flimlem  19482  mbfmullem  19485  itg2const  19500  itg2mulc  19507  itg2monolem1  19510  itg2i1fseqle  19514  itg2i1fseq  19515  itg2addlem  19518  itg2cnlem1  19521  itg2cn  19523  isibl  19525  isibl2  19526  iblitg  19528  itgz  19540  itgvallem  19544  itgvallem3  19545  iblcnlem1  19547  itgcnlem  19549  iblrelem  19550  iblposlem  19551  iblpos  19552  itgrevallem1  19554  itgposval  19555  iblss2  19565  itgss  19571  itgfsum  19586  iblabslem  19587  iblmulc2  19590  bddmulibl  19598  itgcn  19602  ellimc  19628  dvnfval  19676  cpnfval  19686  dvexp  19707  dvexp2  19708  dvmptfsum  19727  dvlipcn  19746  dvivthlem1  19760  dvfsumle  19773  dvfsumabs  19775  dvfsumlem2  19779  evlslem3  19803  evlslem1  19804  mpfrcl  19807  evlsval  19808  evlsvar  19812  mpfind  19833  pf1ind  19843  elply2  19983  elplyr  19988  elplyd  19989  coeeu  20012  coelem  20013  coeeq  20014  plyco  20028  coe11  20039  coe1termlem  20044  dgrcolem1  20059  dvply2g  20070  elqaalem3  20106  eltayl  20144  tayl0  20146  taylthlem1  20157  taylthlem2  20158  ulmcau  20179  ulmdvlem1  20184  ulmdvlem3  20186  mtest  20188  mtestbdd  20189  pserval  20194  pserulm  20206  psercn  20210  pserdvlem2  20212  abelthlem3  20217  logtayl  20419  dvcxp1  20494  dmarea  20664  musum  20844  dchrptlem2  20917  dchrptlem3  20918  dchrpt  20919  lgsval  20952  lgsval4lem  20959  lgsneg  20971  lgsmod  20973  rpvmasum2  21074  padicfval  21178  ostth2  21199  ostth3  21200  ostth  21201  htthlem  22269  htth  22270  pjhfval  22747  hosmval  23087  hommval  23088  hodmval  23089  hfsmval  23090  hfmmval  23091  brafval  23295  kbfval  23304  indval  24208  ofceq  24277  itgeq12dv  24436  ballotlemfval  24527  lgamgulmlem2  24594  lgamgulmlem5  24597  ptpcon  24700  cvmliftlem15  24765  cvmlift2lem4  24773  cvmlift2  24783  snmlval  24798  snmlflim  24799  relexp0  24909  relexpsucr  24910  prodeq2w  25018  prodmo  25042  fprod  25047  faclim  25124  faclim2  25126  trpredeq1  25248  trpredeq2  25249  bpolylem  25809  voliunnfl  25956  itg2addnclem  25958  itg2gt0cn  25961  iblabsnclem  25969  iblmulc2nc  25971  upixp  26123  rrncmslem  26233  ismrer1  26239  mzpclval  26474  mzpcl2  26479  mzpexpmpt  26494  mzpsubst  26497  mzpcompact2lem  26500  rmxfval  26659  rmyfval  26660  aomclem8  26829  frlmgsum  26902  uvcval  26904  hbtlem1  26997  hbtlem7  26999  pmtrval  27064  mamuval  27114  mamufv  27115  mdetleib  27158  expgrowthi  27220  expgrowth  27222  addrval  27340  subrval  27341  mulvval  27342  fmulcl  27380  fmuldfeqlem1  27381  stoweidlem2  27420  stoweidlem17  27435  stoweidlem19  27437  stoweidlem20  27438  stoweidlem43  27461  stoweidlem62  27480  stoweid  27481  tendoplcbv  30890  tendopl  30891  tendoicbv  30908  tendoi  30909  dihfval  31347  lcfl7N  31617  lcfrlem8  31665  lcfrlem9  31666  lcf1o  31667  hvmapval  31876  hdmap1fval  31913  hdmapffval  31945  hdmapfval  31946  hgmapffval  32004  hgmapfval  32005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-ral 2655  df-opab 4209  df-mpt 4210
  Copyright terms: Public domain W3C validator