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

Theorem mpteq2dv 4296
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 4295 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 4266
This theorem is referenced by:  ofeq  6307  rdgeq1  6669  rdgeq2  6670  omv  6756  oev  6758  oieq1  7481  oieq2  7482  cantnflem1  7645  wunex2  8613  wuncval2  8622  reexALT  10606  seqof2  11381  limsupval  12268  sumeq2w  12486  cbvsum  12489  summo  12511  fsum  12514  fsumrlim  12590  fsumo1  12591  rpnnen2lem1  12814  rpnnen2lem2  12815  rpnnen  12826  1arithlem1  13291  vdwapval  13341  vdwlem6  13354  vdwlem8  13356  vdwlem9  13357  vdwlem10  13358  ramub1lem2  13395  ramcl  13397  prdsplusgval  13695  prdsmulrval  13697  prdsdsval  13700  prdsvscaval  13701  ismon  13959  fucco  14159  curf1  14322  curf2  14326  yonedalem4a  14372  grplactfval  14885  galactghm  15106  sylow1  15237  sylow2b  15257  sylow3lem5  15265  sylow3  15267  iscyg  15489  gsumzaddlem  15526  gsumzmhm  15533  ablfac2  15647  gsumdixp  15715  psrmulfval  16449  mvrval  16485  subrgmvr  16524  mplcoe1  16528  mplcoe3  16529  mplcoe2  16530  mplmon2  16553  subrgascl  16558  evlslem2  16568  coe1fval  16603  zncyg  16829  phllmhm  16863  isphld  16885  ptbasfi  17613  ptcnplem  17653  ptrescn  17671  cnmpt2k  17720  xkohmeo  17847  fmval  17975  fmf  17977  ptcmpg  18088  tmdmulg  18122  prdstmdd  18153  tsmspropd  18161  prdsxmslem2  18559  metdsval  18877  fsumcn  18900  expcn  18902  lebnumlem3  18988  pcoval  19036  pi1xfrcnv  19082  itg11  19583  mbfi1fseqlem2  19608  mbfi1fseqlem6  19612  mbfi1fseq  19613  mbfi1flimlem  19614  mbfmullem  19617  itg2const  19632  itg2mulc  19639  itg2monolem1  19642  itg2i1fseqle  19646  itg2i1fseq  19647  itg2addlem  19650  itg2cnlem1  19653  itg2cn  19655  isibl  19657  isibl2  19658  iblitg  19660  itgz  19672  itgvallem  19676  itgvallem3  19677  iblcnlem1  19679  itgcnlem  19681  iblrelem  19682  iblposlem  19683  iblpos  19684  itgrevallem1  19686  itgposval  19687  iblss2  19697  itgss  19703  itgfsum  19718  iblabslem  19719  iblmulc2  19722  bddmulibl  19730  itgcn  19734  ellimc  19760  dvnfval  19808  cpnfval  19818  dvexp  19839  dvexp2  19840  dvmptfsum  19859  dvlipcn  19878  dvivthlem1  19892  dvfsumle  19905  dvfsumabs  19907  dvfsumlem2  19911  evlslem3  19935  evlslem1  19936  mpfrcl  19939  evlsval  19940  evlsvar  19944  mpfind  19965  pf1ind  19975  elply2  20115  elplyr  20120  elplyd  20121  coeeu  20144  coelem  20145  coeeq  20146  plyco  20160  coe11  20171  coe1termlem  20176  dgrcolem1  20191  dvply2g  20202  elqaalem3  20238  eltayl  20276  tayl0  20278  taylthlem1  20289  taylthlem2  20290  ulmcau  20311  ulmdvlem1  20316  ulmdvlem3  20318  mtest  20320  mtestbdd  20321  pserval  20326  pserulm  20338  psercn  20342  pserdvlem2  20344  abelthlem3  20349  logtayl  20551  dvcxp1  20626  dmarea  20796  musum  20976  dchrptlem2  21049  dchrptlem3  21050  dchrpt  21051  lgsval  21084  lgsval4lem  21091  lgsneg  21103  lgsmod  21105  rpvmasum2  21206  padicfval  21310  ostth2  21331  ostth3  21332  ostth  21333  htthlem  22420  htth  22421  pjhfval  22898  hosmval  23238  hommval  23239  hodmval  23240  hfsmval  23241  hfmmval  23242  brafval  23446  kbfval  23455  indval  24411  ofceq  24480  itgeq12dv  24641  ballotlemfval  24747  lgamgulmlem2  24814  lgamgulmlem5  24817  ptpcon  24920  cvmliftlem15  24985  cvmlift2lem4  24993  cvmlift2  25003  snmlval  25018  snmlflim  25019  relexp0  25129  relexpsucr  25130  prodeq2w  25238  prodmo  25262  fprod  25267  faclim  25365  faclim2  25367  trpredeq1  25498  trpredeq2  25499  bpolylem  26094  voliunnfl  26250  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  iblabsnclem  26268  iblmulc2nc  26270  ftc1anclem2  26281  ftc1anclem6  26285  ftc1anclem8  26287  ftc1anc  26288  ftc2nc  26289  upixp  26431  rrncmslem  26541  ismrer1  26547  mzpclval  26782  mzpcl2  26787  mzpexpmpt  26802  mzpsubst  26805  mzpcompact2lem  26808  rmxfval  26967  rmyfval  26968  aomclem8  27136  frlmgsum  27209  uvcval  27211  hbtlem1  27304  hbtlem7  27306  pmtrval  27371  mamuval  27421  mamufv  27422  mdetleib  27465  expgrowthi  27527  expgrowth  27529  addrval  27647  subrval  27648  mulvval  27649  fmulcl  27687  fmuldfeqlem1  27688  stoweidlem2  27727  stoweidlem17  27742  stoweidlem19  27744  stoweidlem20  27745  stoweidlem43  27768  stoweidlem62  27787  stoweid  27788  tendoplcbv  31572  tendopl  31573  tendoicbv  31590  tendoi  31591  dihfval  32029  lcfl7N  32299  lcfrlem8  32347  lcfrlem9  32348  lcf1o  32349  hvmapval  32558  hdmap1fval  32595  hdmapffval  32627  hdmapfval  32628  hgmapffval  32686  hgmapfval  32687
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-ral 2710  df-opab 4267  df-mpt 4268
  Copyright terms: Public domain W3C validator