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

Theorem imaeq1d 5205
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 5201 . 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 1653   "cima 4884
This theorem is referenced by:  imaeq12d  5207  nfimad  5215  f1imacnv  5694  foimacnv  5695  suppssof1  6349  seqomeq12  6714  ssenen  7284  fipreima  7415  oieq1  7484  oieq2  7485  wemapso2  7524  cantnfs  7624  cantnfval  7626  oemapso  7641  mapfien  7656  dfac12lem1  8028  dfac12r  8031  fpwwe2cbv  8510  fpwwe2lem2  8512  fpwwecbv  8524  fpwwelem  8525  seqeq1  11331  seqeq2  11332  seqeq3  11333  1arith  13300  vdwmc  13351  vdwnnlem1  13368  ramub2  13387  rami  13388  imasless  13770  gsumvalx  14779  eqglact  14996  gsumval3  15519  dprdw  15573  rrgsupp  16356  psrbag  16436  psrbagaddcl  16440  psrbaglefi  16442  mplelbas  16499  mplsubglem  16503  mpllsslem  16504  mplsubrg  16508  ltbwe  16538  evlslem4  16569  evlslem2  16573  coe1sfi  16615  ply1coe  16689  iscn  17304  ptbasfi  17618  ptval2  17638  ptrescn  17676  xkoptsub  17691  qtopval  17732  cmphaushmeo  17837  ptcmpg  18093  restutopopn  18273  prdsxmslem2  18564  metuvalOLD  18584  metuval  18585  nghmfval  18761  isnghm  18762  ismbf1  19521  ismbf  19525  mbfconst  19530  mbfres2  19540  cncombf  19553  isi1f  19569  itg1val  19578  evlslem6  19939  tdeglem4  19988  mdegval  19991  mdeg0  19998  mdegvsca  20004  deg1val  20024  deg1mul3  20043  fta1glem2  20094  fta1g  20095  fta1b  20097  plypf1  20136  dgrval  20152  dgrlem  20153  coeidlem  20161  coe11  20176  fta1lem  20229  fta1  20230  vieta1lem2  20233  vieta1  20234  taylthlem2  20295  areaval  20808  jensen  20832  sqff1o  20970  nlfnval  23389  fimacnvinrn  24052  xppreima2  24065  ofpreima  24086  xrhval  24389  indf1ofs  24428  ismbfm  24607  mbfmcst  24614  issibf  24653  sitgfval  24660  ballotlemscr  24781  ballotlemrv  24782  ballotlemrinv0  24795  iscvm  24951  cvmliftmolem1  24973  cvmlift2lem9a  24995  cvmlift2lem9  25003  cnambfre  26266  itg2addnclem2  26270  ftc1anclem1  26293  ftc1anclem6  26298  pw2f1o2val  27123  aomclem8  27149  frlmelbas  27214  frlmssuvc1  27236  frlmssuvc2  27237  frlmsslsp  27238  frlmup1  27240  frlmup3  27242  ellspd  27244  pwfi2f1o  27250  islindf4  27298  psgnunilem1  27406  lkrval  29959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-cnv 4889  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894
  Copyright terms: Public domain W3C validator