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

Theorem imaeq1d 5193
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 5189 . 2  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A " C
)  =  ( B
" C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   "cima 4872
This theorem is referenced by:  imaeq12d  5195  nfimad  5203  f1imacnv  5682  foimacnv  5683  suppssof1  6337  seqomeq12  6702  ssenen  7272  fipreima  7403  oieq1  7470  oieq2  7471  wemapso2  7510  cantnfs  7610  cantnfval  7612  oemapso  7627  mapfien  7642  dfac12lem1  8012  dfac12r  8015  fpwwe2cbv  8494  fpwwe2lem2  8496  fpwwecbv  8508  fpwwelem  8509  seqeq1  11314  seqeq2  11315  seqeq3  11316  1arith  13283  vdwmc  13334  vdwnnlem1  13351  ramub2  13370  rami  13371  imasless  13753  gsumvalx  14762  eqglact  14979  gsumval3  15502  dprdw  15556  rrgsupp  16339  psrbag  16419  psrbagaddcl  16423  psrbaglefi  16425  mplelbas  16482  mplsubglem  16486  mpllsslem  16487  mplsubrg  16491  ltbwe  16521  evlslem4  16552  evlslem2  16556  coe1sfi  16598  ply1coe  16672  iscn  17287  ptbasfi  17601  ptval2  17621  ptrescn  17659  xkoptsub  17674  qtopval  17715  cmphaushmeo  17820  ptcmpg  18076  restutopopn  18256  prdsxmslem2  18547  metuvalOLD  18567  metuval  18568  nghmfval  18744  isnghm  18745  ismbf1  19506  ismbf  19510  mbfconst  19515  mbfres2  19525  cncombf  19538  isi1f  19554  itg1val  19563  evlslem6  19922  tdeglem4  19971  mdegval  19974  mdeg0  19981  mdegvsca  19987  deg1val  20007  deg1mul3  20026  fta1glem2  20077  fta1g  20078  fta1b  20080  plypf1  20119  dgrval  20135  dgrlem  20136  coeidlem  20144  coe11  20159  fta1lem  20212  fta1  20213  vieta1lem2  20216  vieta1  20217  taylthlem2  20278  areaval  20791  jensen  20815  sqff1o  20953  nlfnval  23372  fimacnvinrn  24035  xppreima2  24048  ofpreima  24069  xrhval  24372  indf1ofs  24411  ismbfm  24590  mbfmcst  24597  issibf  24636  sitgfval  24643  ballotlemscr  24764  ballotlemrv  24765  ballotlemrinv0  24778  iscvm  24934  cvmliftmolem1  24956  cvmlift2lem9a  24978  cvmlift2lem9  24986  predeq1  25424  cnambfre  26201  itg2addnclem2  26203  pw2f1o2val  27047  aomclem8  27074  frlmelbas  27139  frlmssuvc1  27161  frlmssuvc2  27162  frlmsslsp  27163  frlmup1  27165  frlmup3  27167  ellspd  27169  pwfi2f1o  27175  islindf4  27223  psgnunilem1  27331  lkrval  29725
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-cnv 4877  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882
  Copyright terms: Public domain W3C validator