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

Theorem mpteq2dv 4298
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 453 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
32mpteq2dva 4297 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726    e. cmpt 4268
This theorem is referenced by:  ofeq  6309  rdgeq1  6671  rdgeq2  6672  omv  6758  oev  6760  oieq1  7483  oieq2  7484  cantnflem1  7647  wunex2  8615  wuncval2  8624  reexALT  10608  seqof2  11383  limsupval  12270  sumeq2w  12488  cbvsum  12491  summo  12513  fsum  12516  fsumrlim  12592  fsumo1  12593  rpnnen2lem1  12816  rpnnen2lem2  12817  rpnnen  12828  1arithlem1  13293  vdwapval  13343  vdwlem6  13356  vdwlem8  13358  vdwlem9  13359  vdwlem10  13360  ramub1lem2  13397  ramcl  13399  prdsplusgval  13697  prdsmulrval  13699  prdsdsval  13702  prdsvscaval  13703  ismon  13961  fucco  14161  curf1  14324  curf2  14328  yonedalem4a  14374  grplactfval  14887  galactghm  15108  sylow1  15239  sylow2b  15259  sylow3lem5  15267  sylow3  15269  iscyg  15491  gsumzaddlem  15528  gsumzmhm  15535  ablfac2  15649  gsumdixp  15717  psrmulfval  16451  mvrval  16487  subrgmvr  16526  mplcoe1  16530  mplcoe3  16531  mplcoe2  16532  mplmon2  16555  subrgascl  16560  evlslem2  16570  coe1fval  16605  zncyg  16831  phllmhm  16865  isphld  16887  ptbasfi  17615  ptcnplem  17655  ptrescn  17673  cnmpt2k  17722  xkohmeo  17849  fmval  17977  fmf  17979  ptcmpg  18090  tmdmulg  18124  prdstmdd  18155  tsmspropd  18163  prdsxmslem2  18561  metdsval  18879  fsumcn  18902  expcn  18904  lebnumlem3  18990  pcoval  19038  pi1xfrcnv  19084  itg11  19585  mbfi1fseqlem2  19610  mbfi1fseqlem6  19614  mbfi1fseq  19615  mbfi1flimlem  19616  mbfmullem  19619  itg2const  19634  itg2mulc  19641  itg2monolem1  19644  itg2i1fseqle  19648  itg2i1fseq  19649  itg2addlem  19652  itg2cnlem1  19655  itg2cn  19657  isibl  19659  isibl2  19660  iblitg  19662  itgz  19674  itgvallem  19678  itgvallem3  19679  iblcnlem1  19681  itgcnlem  19683  iblrelem  19684  iblposlem  19685  iblpos  19686  itgrevallem1  19688  itgposval  19689  iblss2  19699  itgss  19705  itgfsum  19720  iblabslem  19721  iblmulc2  19724  bddmulibl  19732  itgcn  19736  ellimc  19762  dvnfval  19810  cpnfval  19820  dvexp  19841  dvexp2  19842  dvmptfsum  19861  dvlipcn  19880  dvivthlem1  19894  dvfsumle  19907  dvfsumabs  19909  dvfsumlem2  19913  evlslem3  19937  evlslem1  19938  mpfrcl  19941  evlsval  19942  evlsvar  19946  mpfind  19967  pf1ind  19977  elply2  20117  elplyr  20122  elplyd  20123  coeeu  20146  coelem  20147  coeeq  20148  plyco  20162  coe11  20173  coe1termlem  20178  dgrcolem1  20193  dvply2g  20204  elqaalem3  20240  eltayl  20278  tayl0  20280  taylthlem1  20291  taylthlem2  20292  ulmcau  20313  ulmdvlem1  20318  ulmdvlem3  20320  mtest  20322  mtestbdd  20323  pserval  20328  pserulm  20340  psercn  20344  pserdvlem2  20346  abelthlem3  20351  logtayl  20553  dvcxp1  20628  dmarea  20798  musum  20978  dchrptlem2  21051  dchrptlem3  21052  dchrpt  21053  lgsval  21086  lgsval4lem  21093  lgsneg  21105  lgsmod  21107  rpvmasum2  21208  padicfval  21312  ostth2  21333  ostth3  21334  ostth  21335  htthlem  22422  htth  22423  pjhfval  22900  hosmval  23240  hommval  23241  hodmval  23242  hfsmval  23243  hfmmval  23244  brafval  23448  kbfval  23457  indval  24413  ofceq  24482  itgeq12dv  24643  ballotlemfval  24749  lgamgulmlem2  24816  lgamgulmlem5  24819  ptpcon  24922  cvmliftlem15  24987  cvmlift2lem4  24995  cvmlift2  25005  snmlval  25020  snmlflim  25021  relexp0  25131  relexpsucr  25132  prodeq2w  25240  prodmo  25264  fprod  25269  faclim  25367  faclim2  25369  trpredeq1  25500  trpredeq2  25501  bpolylem  26096  voliunnfl  26252  itg2addnclem  26258  itg2addnclem3  26260  itg2addnc  26261  itg2gt0cn  26262  iblabsnclem  26270  iblmulc2nc  26272  ftc1anclem2  26283  ftc1anclem6  26287  ftc1anclem8  26289  ftc1anc  26290  ftc2nc  26291  upixp  26433  rrncmslem  26543  ismrer1  26549  mzpclval  26784  mzpcl2  26789  mzpexpmpt  26804  mzpsubst  26807  mzpcompact2lem  26810  rmxfval  26969  rmyfval  26970  aomclem8  27138  frlmgsum  27211  uvcval  27213  hbtlem1  27306  hbtlem7  27308  pmtrval  27373  mamuval  27423  mamufv  27424  mdetleib  27467  expgrowthi  27529  expgrowth  27531  addrval  27649  subrval  27650  mulvval  27651  fmulcl  27689  fmuldfeqlem1  27690  stoweidlem2  27729  stoweidlem17  27744  stoweidlem19  27746  stoweidlem20  27747  stoweidlem43  27770  stoweidlem62  27789  stoweid  27790  wwlkn  28352  tendoplcbv  31634  tendopl  31635  tendoicbv  31652  tendoi  31653  dihfval  32091  lcfl7N  32361  lcfrlem8  32409  lcfrlem9  32410  lcf1o  32411  hvmapval  32620  hdmap1fval  32657  hdmapffval  32689  hdmapfval  32690  hgmapffval  32748  hgmapfval  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-opab 4269  df-mpt 4270
  Copyright terms: Public domain W3C validator