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

Theorem imaeq1d 5165
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 5161 . 2  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A " C
)  =  ( B
" C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   "cima 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-cnv 4844  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849
This theorem is referenced by:  imaeq12d  5167  nfimad  5175  csbrn  5296  f1imacnv  5654  foimacnv  5655  suppssof1OLD  6338  seqomeq12  6905  ssenen  7481  fipreima  7613  oieq1  7722  oieq2  7723  wemapso2OLD  7762  cantnfsOLD  7900  cantnfvalOLD  7902  mapfienOLD  7923  dfac12lem1  8308  dfac12r  8311  fpwwe2cbv  8793  fpwwe2lem2  8795  fpwwecbv  8807  fpwwelem  8808  seqeq1  11805  seqeq2  11806  seqeq3  11807  1arith  13984  vdwmc  14035  vdwnnlem1  14052  ramub2  14071  rami  14072  imasless  14474  gsumvalx  15497  eqglact  15725  psgnunilem1  15992  gsumval3OLD  16375  dprdwOLD  16490  rrgsuppOLD  17341  psrbag  17421  psrbagaddclOLD  17429  psrbaglefi  17431  psrbaglefiOLD  17432  mplelbasOLD  17496  mplsubglemOLD  17502  mpllsslemOLD  17503  evlslem4OLD  17574  coe1sfiOLD  17624  evpmss  17916  psgnevpmb  17917  frlmelbasOLD  18083  frlmssuvc1OLD  18121  frlmssuvc2OLD  18122  frlmsslspOLD  18124  frlmup3  18128  ellspdOLD  18131  iscn  18739  ptbasfi  19054  ptval2  19074  ptrescn  19112  xkoptsub  19127  qtopval  19168  cmphaushmeo  19273  ptcmpg  19529  restutopopn  19713  prdsxmslem2  20004  metuvalOLD  20024  metuval  20025  nghmfval  20201  isnghm  20202  ismbf1  21004  ismbf  21008  mbfconst  21013  mbfres2  21023  cncombf  21036  isi1f  21052  itg1val  21061  evlslem6OLD  21423  mdegvalOLD  21477  deg1val  21510  deg1valOLD  21511  fta1glem2  21581  fta1g  21582  fta1b  21584  dgrval  21639  dgrlem  21640  coeidlem  21648  coe11  21663  fta1lem  21716  fta1  21717  vieta1lem2  21720  vieta1  21721  taylthlem2  21782  areaval  22301  sqff1o  22463  nlfnval  25204  fimacnvinrn  25871  xppreima2  25884  ofpreima  25903  fpwrelmapffslem  25951  xrhval  26364  indf1ofs  26402  ismbfm  26587  mbfmcst  26594  issibf  26633  sitgfval  26641  eulerpartlemelr  26654  eulerpartleme  26660  eulerpartlemo  26662  eulerpartlemt0  26666  eulerpartlemt  26668  eulerpartlemr  26671  eulerpartlemgf  26676  eulerpartlemgs2  26677  eulerpartlemn  26678  eulerpart  26679  ballotlemscr  26815  ballotlemrv  26816  ballotlemrinv0  26829  iscvm  27062  cvmliftmolem1  27084  cvmlift2lem9a  27106  cvmlift2lem9  27114  cnambfre  28349  itg2addnclem2  28353  ftc1anclem1  28376  ftc1anclem6  28381  pw2f1o2val  29297  aomclem8  29323  pwfi2f1o  29360  lkrval  32421
  Copyright terms: Public domain W3C validator