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

Theorem mpteq2dv 4107
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 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
32mpteq2dva 4106 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684    e. cmpt 4077
This theorem is referenced by:  ofeq  6080  rdgeq1  6424  rdgeq2  6425  omv  6511  oev  6513  oieq1  7227  oieq2  7228  cantnflem1  7391  wunex2  8360  reexALT  10348  limsupval  11948  sumeq2w  12165  cbvsum  12168  summo  12190  fsum  12193  fsumrlim  12269  fsumo1  12270  rpnnen2lem1  12493  rpnnen2lem2  12494  rpnnen  12505  1arithlem1  12970  vdwapval  13020  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  vdwlem10  13037  ramub1lem2  13074  ramcl  13076  prdsplusgval  13372  prdsmulrval  13374  prdsdsval  13377  prdsvscaval  13378  yonedalem4a  14049  grplactfval  14562  galactghm  14783  sylow1  14914  sylow2b  14934  sylow3lem5  14942  sylow3  14944  iscyg  15166  gsumzaddlem  15203  gsumzmhm  15210  ablfac2  15324  gsumdixp  15392  psrmulfval  16130  mvrval  16166  subrgmvr  16205  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  mplmon2  16234  subrgascl  16239  evlslem2  16249  coe1fval  16286  zncyg  16502  phllmhm  16536  isphld  16558  ptbasfi  17276  ptcnplem  17315  ptrescn  17333  cnmpt2k  17382  xkohmeo  17506  fmval  17638  fmf  17640  ptcmpg  17751  tmdmulg  17775  prdstmdd  17806  tsmspropd  17814  prdsxmslem2  18075  metdsval  18351  fsumcn  18374  expcn  18376  lebnumlem3  18461  pcoval  18509  pi1xfrcnv  18555  itg11  19046  mbfi1fseqlem2  19071  mbfi1fseqlem6  19075  mbfi1fseq  19076  mbfi1flimlem  19077  mbfmullem  19080  itg2const  19095  itg2mulc  19102  itg2monolem1  19105  itg2i1fseqle  19109  itg2i1fseq  19110  itg2addlem  19113  itg2cnlem1  19116  itg2cn  19118  isibl  19120  isibl2  19121  iblitg  19123  itgz  19135  itgvallem  19139  itgvallem3  19140  iblcnlem1  19142  itgcnlem  19144  iblrelem  19145  iblposlem  19146  iblpos  19147  itgrevallem1  19149  itgposval  19150  iblss2  19160  itgss  19166  itgfsum  19181  iblabslem  19182  iblmulc2  19185  bddmulibl  19193  itgcn  19197  ellimc  19223  dvnfval  19271  cpnfval  19281  dvexp  19302  dvexp2  19303  dvmptfsum  19322  dvlipcn  19341  dvivthlem1  19355  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  evlslem3  19398  evlslem1  19399  mpfrcl  19402  evlsval  19403  evlsvar  19407  mpfind  19428  pf1ind  19438  elply2  19578  elplyr  19583  elplyd  19584  coeeu  19607  coelem  19608  coeeq  19609  plyco  19623  coe11  19634  coe1termlem  19639  dgrcolem1  19654  dvply2g  19665  elqaalem3  19701  eltayl  19739  tayl0  19741  taylthlem1  19752  taylthlem2  19753  ulmcau  19772  ulmdvlem1  19777  ulmdvlem3  19779  mtest  19781  pserval  19786  pserulm  19798  psercn  19802  pserdvlem2  19804  abelthlem3  19809  logtayl  20007  dvcxp1  20082  dmarea  20252  musum  20431  dchrptlem2  20504  dchrptlem3  20505  dchrpt  20506  lgsval  20539  lgsval4lem  20546  lgsneg  20558  lgsmod  20560  rpvmasum2  20661  padicfval  20765  ostth2  20786  ostth3  20787  ostth  20788  htthlem  21497  htth  21498  pjhfval  21975  hosmval  22315  hommval  22316  hodmval  22317  hfsmval  22318  hfmmval  22319  brafval  22523  kbfval  22532  ballotlemfval  23048  itgeq12dv  23196  ofceq  23458  indval  23597  ptpcon  23764  cvmliftlem15  23829  cvmlift2lem4  23837  cvmlift2  23847  snmlval  23914  snmlflim  23915  relexp0  24025  relexpsucr  24026  trpredeq1  24223  trpredeq2  24224  bpolylem  24783  ispr1  25156  isprj1  25163  islimrs  25580  isaddrv  25646  ismulcv  25681  valtar  25883  upixp  26403  rrncmslem  26556  ismrer1  26562  mzpclval  26803  mzpcl2  26808  mzpexpmpt  26823  mzpsubst  26826  mzpcompact2lem  26829  rmxfval  26989  rmyfval  26990  aomclem8  27159  frlmgsum  27232  uvcval  27234  hbtlem1  27327  hbtlem7  27329  pmtrval  27394  mamuval  27444  mamufv  27445  mdetleib  27488  expgrowthi  27550  expgrowth  27552  addrval  27671  subrval  27672  mulvval  27673  fmulcl  27711  fmuldfeqlem1  27712  stoweidlem2  27751  stoweidlem17  27766  stoweidlem19  27768  stoweidlem20  27769  stoweidlem43  27792  stoweidlem62  27811  stoweid  27812  tendoplcbv  30964  tendopl  30965  tendoicbv  30982  tendoi  30983  dihfval  31421  lcfl7N  31691  lcfrlem8  31739  lcfrlem9  31740  lcf1o  31741  hvmapval  31950  hdmap1fval  31987  hdmapffval  32019  hdmapfval  32020  hgmapffval  32078  hgmapfval  32079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator