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

Theorem imaeq1d 5161
Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
Hypothesis
Ref Expression
imaeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
imaeq1d  |-  ( ph  ->  ( A " C
)  =  ( B
" C ) )

Proof of Theorem imaeq1d
StepHypRef Expression
1 imaeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 imaeq1 5157 . 2  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A " C
)  =  ( B
" C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   "cima 4840
This theorem is referenced by:  imaeq12d  5163  nfimad  5171  f1imacnv  5650  foimacnv  5651  suppssof1  6305  seqomeq12  6670  ssenen  7240  fipreima  7370  oieq1  7437  oieq2  7438  wemapso2  7477  cantnfs  7577  cantnfval  7579  oemapso  7594  mapfien  7609  dfac12lem1  7979  dfac12r  7982  fpwwe2cbv  8461  fpwwe2lem2  8463  fpwwecbv  8475  fpwwelem  8476  seqeq1  11281  seqeq2  11282  seqeq3  11283  1arith  13250  vdwmc  13301  vdwnnlem1  13318  ramub2  13337  rami  13338  imasless  13720  gsumvalx  14729  eqglact  14946  gsumval3  15469  dprdw  15523  rrgsupp  16306  psrbag  16386  psrbagaddcl  16390  psrbaglefi  16392  mplelbas  16449  mplsubglem  16453  mpllsslem  16454  mplsubrg  16458  ltbwe  16488  evlslem4  16519  evlslem2  16523  coe1sfi  16565  ply1coe  16639  iscn  17253  ptbasfi  17566  ptval2  17586  ptrescn  17624  xkoptsub  17639  qtopval  17680  cmphaushmeo  17785  ptcmpg  18041  restutopopn  18221  prdsxmslem2  18512  metuvalOLD  18532  metuval  18533  nghmfval  18709  isnghm  18710  ismbf1  19471  ismbf  19475  mbfconst  19480  mbfres2  19490  cncombf  19503  isi1f  19519  itg1val  19528  evlslem6  19887  tdeglem4  19936  mdegval  19939  mdeg0  19946  mdegvsca  19952  deg1val  19972  deg1mul3  19991  fta1glem2  20042  fta1g  20043  fta1b  20045  plypf1  20084  dgrval  20100  dgrlem  20101  coeidlem  20109  coe11  20124  fta1lem  20177  fta1  20178  vieta1lem2  20181  vieta1  20182  taylthlem2  20243  areaval  20756  jensen  20780  sqff1o  20918  nlfnval  23337  fimacnvinrn  24000  xppreima2  24013  ofpreima  24034  xrhval  24337  indf1ofs  24376  ismbfm  24555  mbfmcst  24562  issibf  24601  sitgfval  24608  ballotlemscr  24729  ballotlemrv  24730  ballotlemrinv0  24743  iscvm  24899  cvmliftmolem1  24921  cvmlift2lem9a  24943  cvmlift2lem9  24951  predeq1  25383  cnambfre  26154  itg2addnclem2  26156  pw2f1o2val  27000  aomclem8  27027  frlmelbas  27092  frlmssuvc1  27114  frlmssuvc2  27115  frlmsslsp  27116  frlmup1  27118  frlmup3  27120  ellspd  27122  pwfi2f1o  27128  islindf4  27176  psgnunilem1  27284  lkrval  29571
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-cnv 4845  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850
  Copyright terms: Public domain W3C validator