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

Theorem imaeq1d 5187
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 5183 . 2  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
31, 2syl 17 1  |-  ( ph  ->  ( A " C
)  =  ( B
" C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   "cima 4857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-cnv 4862  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867
This theorem is referenced by:  imaeq12d  5189  nfimad  5197  csbrn  5317  f1imacnv  5847  foimacnv  5848  seqomeq12  7179  ssenen  7752  fipreima  7886  oieq1  8027  oieq2  8028  dfac12lem1  8571  dfac12r  8574  fpwwe2cbv  9054  fpwwe2lem2  9056  fpwwecbv  9068  fpwwelem  9069  seqeq1  12213  seqeq2  12214  seqeq3  12215  1arith  14834  vdwmc  14891  vdwnnlem1  14908  ramub2  14934  rami  14935  imasless  15397  gsumvalx  16464  eqglact  16819  psgnunilem1  17085  psrbag  18523  psrbaglefi  18531  evpmss  19085  psgnevpmb  19086  frlmup3  19289  iscn  20182  ptbasfi  20527  ptval2  20547  ptrescn  20585  xkoptsub  20600  qtopval  20641  cmphaushmeo  20746  ptcmpg  21003  restutopopn  21184  prdsxmslem2  21475  metuval  21495  nghmfval  21654  isnghm  21655  ismbf1  22459  ismbf  22463  mbfconst  22468  mbfres2  22478  cncombf  22491  isi1f  22509  itg1val  22518  deg1val  22922  fta1glem2  22992  fta1g  22993  fta1b  22995  dgrval  23050  dgrlem  23051  coeidlem  23059  coe11  23075  fta1lem  23128  fta1  23129  vieta1lem2  23132  vieta1  23133  taylthlem2  23194  areaval  23755  sqff1o  23972  nlfnval  27369  fimacnvinrn  28075  xppreima2  28089  ofpreima  28108  fpwrelmapffslem  28160  xrhval  28661  indf1ofs  28686  ismbfm  28913  mbfmcst  28920  issibf  28994  sitgfval  29002  eulerpartlemelr  29016  eulerpartleme  29022  eulerpartlemo  29024  eulerpartlemt0  29028  eulerpartlemt  29030  eulerpartlemr  29033  eulerpartlemgf  29038  eulerpartlemgs2  29039  eulerpartlemn  29040  eulerpart  29041  ballotlemscr  29177  ballotlemrv  29178  ballotlemrinv0  29191  iscvm  29770  cvmliftmolem1  29792  cvmlift2lem9a  29814  cvmlift2lem9  29822  msrfval  29963  ismfs  29975  mthmval  30001  poimirlem4  31647  poimirlem5  31648  poimirlem6  31649  poimirlem7  31650  poimirlem8  31651  poimirlem10  31653  poimirlem11  31654  poimirlem12  31655  poimirlem13  31656  poimirlem14  31657  poimirlem15  31658  poimirlem16  31659  poimirlem17  31660  poimirlem18  31661  poimirlem19  31662  poimirlem20  31663  poimirlem21  31664  poimirlem22  31665  poimirlem26  31669  poimirlem27  31670  poimirlem32  31675  cnambfre  31692  itg2addnclem2  31697  ftc1anclem1  31720  ftc1anclem6  31725  lkrval  32362  pw2f1o2val  35599  aomclem8  35624  pwfi2f1o  35659  trclimalb2  35956  frege131d  35994  dirkercncflem2  37534
  Copyright terms: Public domain W3C validator