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

Theorem imaeq1d 5168
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 5164 . 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 1369   "cima 4843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-cnv 4848  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853
This theorem is referenced by:  imaeq12d  5170  nfimad  5178  csbrn  5299  f1imacnv  5657  foimacnv  5658  suppssof1OLD  6339  seqomeq12  6909  ssenen  7485  fipreima  7617  oieq1  7726  oieq2  7727  wemapso2OLD  7766  cantnfsOLD  7904  cantnfvalOLD  7906  mapfienOLD  7927  dfac12lem1  8312  dfac12r  8315  fpwwe2cbv  8797  fpwwe2lem2  8799  fpwwecbv  8811  fpwwelem  8812  seqeq1  11809  seqeq2  11810  seqeq3  11811  1arith  13988  vdwmc  14039  vdwnnlem1  14056  ramub2  14075  rami  14076  imasless  14478  gsumvalx  15502  eqglact  15732  psgnunilem1  15999  gsumval3OLD  16382  dprdwOLD  16500  rrgsuppOLD  17363  psrbag  17431  psrbagaddclOLD  17439  psrbaglefi  17441  psrbaglefiOLD  17442  mplelbasOLD  17506  mplsubglemOLD  17512  mpllsslemOLD  17513  evlslem4OLD  17590  evlslem6OLD  17599  coe1sfiOLD  17669  evpmss  18016  psgnevpmb  18017  frlmelbasOLD  18183  frlmssuvc1OLD  18221  frlmssuvc2OLD  18222  frlmsslspOLD  18224  frlmup3  18228  ellspdOLD  18231  iscn  18839  ptbasfi  19154  ptval2  19174  ptrescn  19212  xkoptsub  19227  qtopval  19268  cmphaushmeo  19373  ptcmpg  19629  restutopopn  19813  prdsxmslem2  20104  metuvalOLD  20124  metuval  20125  nghmfval  20301  isnghm  20302  ismbf1  21104  ismbf  21108  mbfconst  21113  mbfres2  21123  cncombf  21136  isi1f  21152  itg1val  21161  mdegvalOLD  21534  deg1val  21567  deg1valOLD  21568  fta1glem2  21638  fta1g  21639  fta1b  21641  dgrval  21696  dgrlem  21697  coeidlem  21705  coe11  21720  fta1lem  21773  fta1  21774  vieta1lem2  21777  vieta1  21778  taylthlem2  21839  areaval  22358  sqff1o  22520  nlfnval  25285  fimacnvinrn  25952  xppreima2  25965  ofpreima  25984  fpwrelmapffslem  26032  xrhval  26444  indf1ofs  26482  ismbfm  26667  mbfmcst  26674  issibf  26719  sitgfval  26727  eulerpartlemelr  26740  eulerpartleme  26746  eulerpartlemo  26748  eulerpartlemt0  26752  eulerpartlemt  26754  eulerpartlemr  26757  eulerpartlemgf  26762  eulerpartlemgs2  26763  eulerpartlemn  26764  eulerpart  26765  ballotlemscr  26901  ballotlemrv  26902  ballotlemrinv0  26915  iscvm  27148  cvmliftmolem1  27170  cvmlift2lem9a  27192  cvmlift2lem9  27200  cnambfre  28440  itg2addnclem2  28444  ftc1anclem1  28467  ftc1anclem6  28472  pw2f1o2val  29388  aomclem8  29414  pwfi2f1o  29451  lkrval  32733
  Copyright terms: Public domain W3C validator