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

Theorem imaeq1d 5336
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 5332 . 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 1379   "cima 5002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012
This theorem is referenced by:  imaeq12d  5338  nfimad  5346  csbrn  5468  f1imacnv  5832  foimacnv  5833  suppssof1OLD  6543  seqomeq12  7119  ssenen  7691  fipreima  7826  oieq1  7937  oieq2  7938  wemapso2OLD  7977  cantnfsOLD  8115  cantnfvalOLD  8117  mapfienOLD  8138  dfac12lem1  8523  dfac12r  8526  fpwwe2cbv  9008  fpwwe2lem2  9010  fpwwecbv  9022  fpwwelem  9023  seqeq1  12078  seqeq2  12079  seqeq3  12080  1arith  14304  vdwmc  14355  vdwnnlem1  14372  ramub2  14391  rami  14392  imasless  14795  gsumvalx  15824  eqglact  16057  psgnunilem1  16324  gsumval3OLD  16711  dprdwOLD  16852  rrgsuppOLD  17739  psrbag  17812  psrbagaddclOLD  17820  psrbaglefi  17822  psrbaglefiOLD  17823  mplelbasOLD  17888  mplsubglemOLD  17894  mpllsslemOLD  17895  evlslem4OLD  17972  evlslem6OLD  17981  coe1sfiOLD  18052  evpmss  18417  psgnevpmb  18418  frlmelbasOLD  18584  frlmssuvc1OLD  18622  frlmssuvc2OLD  18623  frlmsslspOLD  18625  frlmup3  18629  ellspdOLD  18632  iscn  19530  ptbasfi  19845  ptval2  19865  ptrescn  19903  xkoptsub  19918  qtopval  19959  cmphaushmeo  20064  ptcmpg  20320  restutopopn  20504  prdsxmslem2  20795  metuvalOLD  20815  metuval  20816  nghmfval  20992  isnghm  20993  ismbf1  21796  ismbf  21800  mbfconst  21805  mbfres2  21815  cncombf  21828  isi1f  21844  itg1val  21853  mdegvalOLD  22226  deg1val  22259  deg1valOLD  22260  fta1glem2  22330  fta1g  22331  fta1b  22333  dgrval  22388  dgrlem  22389  coeidlem  22397  coe11  22412  fta1lem  22465  fta1  22466  vieta1lem2  22469  vieta1  22470  taylthlem2  22531  areaval  23050  sqff1o  23212  nlfnval  26504  fimacnvinrn  27176  xppreima2  27188  ofpreima  27207  fpwrelmapffslem  27255  xrhval  27660  indf1ofs  27707  ismbfm  27891  mbfmcst  27898  issibf  27943  sitgfval  27951  eulerpartlemelr  27964  eulerpartleme  27970  eulerpartlemo  27972  eulerpartlemt0  27976  eulerpartlemt  27978  eulerpartlemr  27981  eulerpartlemgf  27986  eulerpartlemgs2  27987  eulerpartlemn  27988  eulerpart  27989  ballotlemscr  28125  ballotlemrv  28126  ballotlemrinv0  28139  iscvm  28372  cvmliftmolem1  28394  cvmlift2lem9a  28416  cvmlift2lem9  28424  cnambfre  29668  itg2addnclem2  29672  ftc1anclem1  29695  ftc1anclem6  29700  pw2f1o2val  30613  aomclem8  30639  pwfi2f1o  30676  dirkercncflem2  31432  lkrval  33903
  Copyright terms: Public domain W3C validator