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

Theorem imaeq1d 5248
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 5244 . 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 1399   "cima 4916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-cnv 4921  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926
This theorem is referenced by:  imaeq12d  5250  nfimad  5258  csbrn  5377  f1imacnv  5740  foimacnv  5741  suppssof1OLD  6458  seqomeq12  7037  ssenen  7610  fipreima  7741  oieq1  7852  oieq2  7853  wemapso2OLD  7892  cantnfsOLD  8028  cantnfvalOLD  8030  mapfienOLD  8051  dfac12lem1  8436  dfac12r  8439  fpwwe2cbv  8919  fpwwe2lem2  8921  fpwwecbv  8933  fpwwelem  8934  seqeq1  12013  seqeq2  12014  seqeq3  12015  1arith  14447  vdwmc  14498  vdwnnlem1  14515  ramub2  14534  rami  14535  imasless  14947  gsumvalx  16014  eqglact  16369  psgnunilem1  16635  gsumval3OLD  17025  dprdwOLD  17163  rrgsuppOLD  18053  psrbag  18126  psrbagaddclOLD  18134  psrbaglefi  18136  psrbaglefiOLD  18137  mplelbasOLD  18202  mplsubglemOLD  18208  mpllsslemOLD  18209  evlslem4OLD  18286  evlslem6OLD  18295  coe1sfiOLD  18366  evpmss  18713  psgnevpmb  18714  frlmup3  18920  iscn  19822  ptbasfi  20167  ptval2  20187  ptrescn  20225  xkoptsub  20240  qtopval  20281  cmphaushmeo  20386  ptcmpg  20642  restutopopn  20826  prdsxmslem2  21117  metuvalOLD  21137  metuval  21138  nghmfval  21314  isnghm  21315  ismbf1  22118  ismbf  22122  mbfconst  22127  mbfres2  22137  cncombf  22150  isi1f  22166  itg1val  22175  mdegvalOLD  22548  deg1val  22581  deg1valOLD  22582  fta1glem2  22652  fta1g  22653  fta1b  22655  dgrval  22710  dgrlem  22711  coeidlem  22719  coe11  22735  fta1lem  22788  fta1  22789  vieta1lem2  22792  vieta1  22793  taylthlem2  22854  areaval  23411  sqff1o  23573  nlfnval  26916  fimacnvinrn  27615  xppreima2  27628  ofpreima  27653  fpwrelmapffslem  27705  xrhval  28149  indf1ofs  28174  ismbfm  28379  mbfmcst  28386  issibf  28458  sitgfval  28466  eulerpartlemelr  28479  eulerpartleme  28485  eulerpartlemo  28487  eulerpartlemt0  28491  eulerpartlemt  28493  eulerpartlemr  28496  eulerpartlemgf  28501  eulerpartlemgs2  28502  eulerpartlemn  28503  eulerpart  28504  ballotlemscr  28640  ballotlemrv  28641  ballotlemrinv0  28654  iscvm  28893  cvmliftmolem1  28915  cvmlift2lem9a  28937  cvmlift2lem9  28945  msrfval  29086  ismfs  29098  mthmval  29124  cnambfre  30228  itg2addnclem2  30233  ftc1anclem1  30256  ftc1anclem6  30261  pw2f1o2val  31147  aomclem8  31173  pwfi2f1o  31210  pwfi2f1oOLD  31211  dirkercncflem2  32052  lkrval  35226  trclimalb2  38257
  Copyright terms: Public domain W3C validator