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

Theorem mpteq2dv 4123
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 4122 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696    e. cmpt 4093
This theorem is referenced by:  ofeq  6096  rdgeq1  6440  rdgeq2  6441  omv  6527  oev  6529  oieq1  7243  oieq2  7244  cantnflem1  7407  wunex2  8376  reexALT  10364  limsupval  11964  sumeq2w  12181  cbvsum  12184  summo  12206  fsum  12209  fsumrlim  12285  fsumo1  12286  rpnnen2lem1  12509  rpnnen2lem2  12510  rpnnen  12521  1arithlem1  12986  vdwapval  13036  vdwlem6  13049  vdwlem8  13051  vdwlem9  13052  vdwlem10  13053  ramub1lem2  13090  ramcl  13092  prdsplusgval  13388  prdsmulrval  13390  prdsdsval  13393  prdsvscaval  13394  yonedalem4a  14065  grplactfval  14578  galactghm  14799  sylow1  14930  sylow2b  14950  sylow3lem5  14958  sylow3  14960  iscyg  15182  gsumzaddlem  15219  gsumzmhm  15226  ablfac2  15340  gsumdixp  15408  psrmulfval  16146  mvrval  16182  subrgmvr  16221  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  mplmon2  16250  subrgascl  16255  evlslem2  16265  coe1fval  16302  zncyg  16518  phllmhm  16552  isphld  16574  ptbasfi  17292  ptcnplem  17331  ptrescn  17349  cnmpt2k  17398  xkohmeo  17522  fmval  17654  fmf  17656  ptcmpg  17767  tmdmulg  17791  prdstmdd  17822  tsmspropd  17830  prdsxmslem2  18091  metdsval  18367  fsumcn  18390  expcn  18392  lebnumlem3  18477  pcoval  18525  pi1xfrcnv  18571  itg11  19062  mbfi1fseqlem2  19087  mbfi1fseqlem6  19091  mbfi1fseq  19092  mbfi1flimlem  19093  mbfmullem  19096  itg2const  19111  itg2mulc  19118  itg2monolem1  19121  itg2i1fseqle  19125  itg2i1fseq  19126  itg2addlem  19129  itg2cnlem1  19132  itg2cn  19134  isibl  19136  isibl2  19137  iblitg  19139  itgz  19151  itgvallem  19155  itgvallem3  19156  iblcnlem1  19158  itgcnlem  19160  iblrelem  19161  iblposlem  19162  iblpos  19163  itgrevallem1  19165  itgposval  19166  iblss2  19176  itgss  19182  itgfsum  19197  iblabslem  19198  iblmulc2  19201  bddmulibl  19209  itgcn  19213  ellimc  19239  dvnfval  19287  cpnfval  19297  dvexp  19318  dvexp2  19319  dvmptfsum  19338  dvlipcn  19357  dvivthlem1  19371  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  evlslem3  19414  evlslem1  19415  mpfrcl  19418  evlsval  19419  evlsvar  19423  mpfind  19444  pf1ind  19454  elply2  19594  elplyr  19599  elplyd  19600  coeeu  19623  coelem  19624  coeeq  19625  plyco  19639  coe11  19650  coe1termlem  19655  dgrcolem1  19670  dvply2g  19681  elqaalem3  19717  eltayl  19755  tayl0  19757  taylthlem1  19768  taylthlem2  19769  ulmcau  19788  ulmdvlem1  19793  ulmdvlem3  19795  mtest  19797  pserval  19802  pserulm  19814  psercn  19818  pserdvlem2  19820  abelthlem3  19825  logtayl  20023  dvcxp1  20098  dmarea  20268  musum  20447  dchrptlem2  20520  dchrptlem3  20521  dchrpt  20522  lgsval  20555  lgsval4lem  20562  lgsneg  20574  lgsmod  20576  rpvmasum2  20677  padicfval  20781  ostth2  20802  ostth3  20803  ostth  20804  htthlem  21513  htth  21514  pjhfval  21991  hosmval  22331  hommval  22332  hodmval  22333  hfsmval  22334  hfmmval  22335  brafval  22539  kbfval  22548  ballotlemfval  23064  itgeq12dv  23211  ofceq  23473  indval  23612  ptpcon  23779  cvmliftlem15  23844  cvmlift2lem4  23852  cvmlift2  23862  snmlval  23929  snmlflim  23930  relexp0  24040  relexpsucr  24041  faclim  24126  cprodeq2w  24134  prodmo  24159  fprod  24164  trpredeq1  24294  trpredeq2  24295  bpolylem  24855  itg2addnclem  25003  itg2gt0cn  25006  iblabsnclem  25014  iblmulc2nc  25016  ispr1  25259  isprj1  25266  islimrs  25683  isaddrv  25749  ismulcv  25784  valtar  25986  upixp  26506  rrncmslem  26659  ismrer1  26665  mzpclval  26906  mzpcl2  26911  mzpexpmpt  26926  mzpsubst  26929  mzpcompact2lem  26932  rmxfval  27092  rmyfval  27093  aomclem8  27262  frlmgsum  27335  uvcval  27337  hbtlem1  27430  hbtlem7  27432  pmtrval  27497  mamuval  27547  mamufv  27548  mdetleib  27591  expgrowthi  27653  expgrowth  27655  addrval  27774  subrval  27775  mulvval  27776  fmulcl  27814  fmuldfeqlem1  27815  stoweidlem2  27854  stoweidlem17  27869  stoweidlem19  27871  stoweidlem20  27872  stoweidlem43  27895  stoweidlem62  27914  stoweid  27915  tendoplcbv  31586  tendopl  31587  tendoicbv  31604  tendoi  31605  dihfval  32043  lcfl7N  32313  lcfrlem8  32361  lcfrlem9  32362  lcf1o  32363  hvmapval  32572  hdmap1fval  32609  hdmapffval  32641  hdmapfval  32642  hgmapffval  32700  hgmapfval  32701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-opab 4094  df-mpt 4095
  Copyright terms: Public domain W3C validator