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

Theorem imaeq1d 5186
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 5182 . 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 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866
This theorem is referenced by:  imaeq12d  5188  nfimad  5196  csbrn  5316  f1imacnv  5847  foimacnv  5848  seqomeq12  7182  ssenen  7755  fipreima  7889  oieq1  8036  oieq2  8037  dfac12lem1  8580  dfac12r  8583  fpwwe2cbv  9062  fpwwe2lem2  9064  fpwwecbv  9076  fpwwelem  9077  seqeq1  12222  seqeq2  12223  seqeq3  12224  1arith  14870  vdwmc  14927  vdwnnlem1  14944  ramub2  14970  rami  14971  imasless  15445  gsumvalx  16512  eqglact  16867  psgnunilem1  17133  psrbag  18587  psrbaglefi  18595  evpmss  19152  psgnevpmb  19153  frlmup3  19356  iscn  20249  ptbasfi  20594  ptval2  20614  ptrescn  20652  xkoptsub  20667  qtopval  20708  cmphaushmeo  20813  ptcmpg  21070  restutopopn  21251  prdsxmslem2  21542  metuval  21562  nghmfval  21725  isnghm  21726  nghmfvalOLD  21743  isnghmOLD  21744  ismbf1  22580  ismbf  22584  mbfconst  22589  mbfres2  22599  cncombf  22612  isi1f  22630  itg1val  22639  deg1val  23043  fta1glem2  23115  fta1g  23116  fta1b  23118  dgrval  23180  dgrlem  23181  coeidlem  23189  coe11  23205  fta1lem  23258  fta1  23259  vieta1lem2  23262  vieta1  23263  taylthlem2  23327  areaval  23888  sqff1o  24107  nlfnval  27532  fimacnvinrn  28237  xppreima2  28251  ofpreima  28270  fpwrelmapffslem  28323  xrhval  28830  indf1ofs  28855  ismbfm  29082  mbfmcst  29089  issibf  29174  sitgfval  29182  eulerpartlemelr  29198  eulerpartleme  29204  eulerpartlemo  29206  eulerpartlemt0  29210  eulerpartlemt  29212  eulerpartlemr  29215  eulerpartlemgf  29220  eulerpartlemgs2  29221  eulerpartlemn  29222  eulerpart  29223  ballotlemscr  29359  ballotlemrv  29360  ballotlemrinv0  29373  ballotlemscrOLD  29397  ballotlemrvOLD  29398  ballotlemrinv0OLD  29411  iscvm  29990  cvmliftmolem1  30012  cvmlift2lem9a  30034  cvmlift2lem9  30042  msrfval  30183  ismfs  30195  mthmval  30221  poimirlem4  31908  poimirlem5  31909  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem10  31914  poimirlem11  31915  poimirlem12  31916  poimirlem13  31917  poimirlem14  31918  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  poimirlem26  31930  poimirlem27  31931  poimirlem32  31936  cnambfre  31953  itg2addnclem2  31958  ftc1anclem1  31981  ftc1anclem6  31986  lkrval  32623  pw2f1o2val  35864  aomclem8  35889  pwfi2f1o  35924  trclimalb2  36288  frege131d  36326  dirkercncflem2  37906
  Copyright terms: Public domain W3C validator