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

Theorem imaeq1d 5143
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 5139 . 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 4822
This theorem is referenced by:  imaeq12d  5145  nfimad  5153  f1imacnv  5632  foimacnv  5633  suppssof1  6286  seqomeq12  6648  ssenen  7218  fipreima  7348  oieq1  7415  oieq2  7416  wemapso2  7455  cantnfs  7555  cantnfval  7557  oemapso  7572  mapfien  7587  dfac12lem1  7957  dfac12r  7960  fpwwe2cbv  8439  fpwwe2lem2  8441  fpwwecbv  8453  fpwwelem  8454  seqeq1  11254  seqeq2  11255  seqeq3  11256  1arith  13223  vdwmc  13274  vdwnnlem1  13291  ramub2  13310  rami  13311  imasless  13693  gsumvalx  14702  eqglact  14919  gsumval3  15442  dprdw  15496  rrgsupp  16279  psrbag  16359  psrbagaddcl  16363  psrbaglefi  16365  mplelbas  16422  mplsubglem  16426  mpllsslem  16427  mplsubrg  16431  ltbwe  16461  evlslem4  16492  evlslem2  16496  coe1sfi  16538  ply1coe  16612  iscn  17222  ptbasfi  17535  ptval2  17555  ptrescn  17593  xkoptsub  17608  qtopval  17649  cmphaushmeo  17754  ptcmpg  18010  restutopopn  18190  prdsxmslem2  18450  metuval  18470  nghmfval  18628  isnghm  18629  ismbf1  19386  ismbf  19390  mbfconst  19395  mbfres2  19405  cncombf  19418  isi1f  19434  itg1val  19443  evlslem6  19802  tdeglem4  19851  mdegval  19854  mdeg0  19861  mdegvsca  19867  deg1val  19887  deg1mul3  19906  fta1glem2  19957  fta1g  19958  fta1b  19960  plypf1  19999  dgrval  20015  dgrlem  20016  coeidlem  20024  coe11  20039  fta1lem  20092  fta1  20093  vieta1lem2  20096  vieta1  20097  taylthlem2  20158  areaval  20671  jensen  20695  sqff1o  20833  nlfnval  23233  fimacnvinrn  23891  xppreima2  23903  indf1ofs  24220  ismbfm  24397  mbfmcst  24404  ballotlemscr  24556  ballotlemrv  24557  ballotlemrinv0  24570  iscvm  24726  cvmliftmolem1  24748  cvmlift2lem9a  24770  cvmlift2lem9  24778  predeq1  25194  itg2addnclem2  25959  pw2f1o2val  26802  aomclem8  26829  frlmelbas  26894  frlmssuvc1  26916  frlmssuvc2  26917  frlmsslsp  26918  frlmup1  26920  frlmup3  26922  ellspd  26924  pwfi2f1o  26930  islindf4  26978  psgnunilem1  27086  lkrval  29204
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-br 4155  df-opab 4209  df-cnv 4827  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832
  Copyright terms: Public domain W3C validator