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

Theorem mpteq2dv 4288
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 4287 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725    e. cmpt 4258
This theorem is referenced by:  ofeq  6298  rdgeq1  6660  rdgeq2  6661  omv  6747  oev  6749  oieq1  7470  oieq2  7471  cantnflem1  7634  wunex2  8602  wuncval2  8611  reexALT  10595  seqof2  11369  limsupval  12256  sumeq2w  12474  cbvsum  12477  summo  12499  fsum  12502  fsumrlim  12578  fsumo1  12579  rpnnen2lem1  12802  rpnnen2lem2  12803  rpnnen  12814  1arithlem1  13279  vdwapval  13329  vdwlem6  13342  vdwlem8  13344  vdwlem9  13345  vdwlem10  13346  ramub1lem2  13383  ramcl  13385  prdsplusgval  13683  prdsmulrval  13685  prdsdsval  13688  prdsvscaval  13689  ismon  13947  fucco  14147  curf1  14310  curf2  14314  yonedalem4a  14360  grplactfval  14873  galactghm  15094  sylow1  15225  sylow2b  15245  sylow3lem5  15253  sylow3  15255  iscyg  15477  gsumzaddlem  15514  gsumzmhm  15521  ablfac2  15635  gsumdixp  15703  psrmulfval  16437  mvrval  16473  subrgmvr  16512  mplcoe1  16516  mplcoe3  16517  mplcoe2  16518  mplmon2  16541  subrgascl  16546  evlslem2  16556  coe1fval  16591  zncyg  16817  phllmhm  16851  isphld  16873  ptbasfi  17601  ptcnplem  17641  ptrescn  17659  cnmpt2k  17708  xkohmeo  17835  fmval  17963  fmf  17965  ptcmpg  18076  tmdmulg  18110  prdstmdd  18141  tsmspropd  18149  prdsxmslem2  18547  metdsval  18865  fsumcn  18888  expcn  18890  lebnumlem3  18976  pcoval  19024  pi1xfrcnv  19070  itg11  19571  mbfi1fseqlem2  19596  mbfi1fseqlem6  19600  mbfi1fseq  19601  mbfi1flimlem  19602  mbfmullem  19605  itg2const  19620  itg2mulc  19627  itg2monolem1  19630  itg2i1fseqle  19634  itg2i1fseq  19635  itg2addlem  19638  itg2cnlem1  19641  itg2cn  19643  isibl  19645  isibl2  19646  iblitg  19648  itgz  19660  itgvallem  19664  itgvallem3  19665  iblcnlem1  19667  itgcnlem  19669  iblrelem  19670  iblposlem  19671  iblpos  19672  itgrevallem1  19674  itgposval  19675  iblss2  19685  itgss  19691  itgfsum  19706  iblabslem  19707  iblmulc2  19710  bddmulibl  19718  itgcn  19722  ellimc  19748  dvnfval  19796  cpnfval  19806  dvexp  19827  dvexp2  19828  dvmptfsum  19847  dvlipcn  19866  dvivthlem1  19880  dvfsumle  19893  dvfsumabs  19895  dvfsumlem2  19899  evlslem3  19923  evlslem1  19924  mpfrcl  19927  evlsval  19928  evlsvar  19932  mpfind  19953  pf1ind  19963  elply2  20103  elplyr  20108  elplyd  20109  coeeu  20132  coelem  20133  coeeq  20134  plyco  20148  coe11  20159  coe1termlem  20164  dgrcolem1  20179  dvply2g  20190  elqaalem3  20226  eltayl  20264  tayl0  20266  taylthlem1  20277  taylthlem2  20278  ulmcau  20299  ulmdvlem1  20304  ulmdvlem3  20306  mtest  20308  mtestbdd  20309  pserval  20314  pserulm  20326  psercn  20330  pserdvlem2  20332  abelthlem3  20337  logtayl  20539  dvcxp1  20614  dmarea  20784  musum  20964  dchrptlem2  21037  dchrptlem3  21038  dchrpt  21039  lgsval  21072  lgsval4lem  21079  lgsneg  21091  lgsmod  21093  rpvmasum2  21194  padicfval  21298  ostth2  21319  ostth3  21320  ostth  21321  htthlem  22408  htth  22409  pjhfval  22886  hosmval  23226  hommval  23227  hodmval  23228  hfsmval  23229  hfmmval  23230  brafval  23434  kbfval  23443  indval  24399  ofceq  24468  itgeq12dv  24629  ballotlemfval  24735  lgamgulmlem2  24802  lgamgulmlem5  24805  ptpcon  24908  cvmliftlem15  24973  cvmlift2lem4  24981  cvmlift2  24991  snmlval  25006  snmlflim  25007  relexp0  25117  relexpsucr  25118  prodeq2w  25227  prodmo  25251  fprod  25256  faclim  25354  faclim2  25356  trpredeq1  25478  trpredeq2  25479  bpolylem  26042  voliunnfl  26196  itg2addnclem  26202  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  iblabsnclem  26214  iblmulc2nc  26216  upixp  26368  rrncmslem  26478  ismrer1  26484  mzpclval  26719  mzpcl2  26724  mzpexpmpt  26739  mzpsubst  26742  mzpcompact2lem  26745  rmxfval  26904  rmyfval  26905  aomclem8  27074  frlmgsum  27147  uvcval  27149  hbtlem1  27242  hbtlem7  27244  pmtrval  27309  mamuval  27359  mamufv  27360  mdetleib  27403  expgrowthi  27465  expgrowth  27467  addrval  27585  subrval  27586  mulvval  27587  fmulcl  27625  fmuldfeqlem1  27626  stoweidlem2  27665  stoweidlem17  27680  stoweidlem19  27682  stoweidlem20  27683  stoweidlem43  27706  stoweidlem62  27725  stoweid  27726  tendoplcbv  31411  tendopl  31412  tendoicbv  31429  tendoi  31430  dihfval  31868  lcfl7N  32138  lcfrlem8  32186  lcfrlem9  32187  lcf1o  32188  hvmapval  32397  hdmap1fval  32434  hdmapffval  32466  hdmapfval  32467  hgmapffval  32525  hgmapfval  32526
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ral 2702  df-opab 4259  df-mpt 4260
  Copyright terms: Public domain W3C validator