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

Theorem imaeq1d 5189
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 5185 . 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 1455   "cima 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419  df-opab 4478  df-cnv 4864  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869
This theorem is referenced by:  imaeq12d  5191  nfimad  5199  csbrn  5320  f1imacnv  5857  foimacnv  5858  seqomeq12  7202  ssenen  7777  fipreima  7911  oieq1  8058  oieq2  8059  dfac12lem1  8604  dfac12r  8607  fpwwe2cbv  9086  fpwwe2lem2  9088  fpwwecbv  9100  fpwwelem  9101  seqeq1  12254  seqeq2  12255  seqeq3  12256  1arith  14926  vdwmc  14983  vdwnnlem1  15000  ramub2  15026  rami  15027  imasless  15501  gsumvalx  16568  eqglact  16923  psgnunilem1  17189  psrbag  18643  psrbaglefi  18651  evpmss  19209  psgnevpmb  19210  frlmup3  19413  iscn  20306  ptbasfi  20651  ptval2  20671  ptrescn  20709  xkoptsub  20724  qtopval  20765  cmphaushmeo  20870  ptcmpg  21127  restutopopn  21308  prdsxmslem2  21599  metuval  21619  nghmfval  21782  isnghm  21783  nghmfvalOLD  21800  isnghmOLD  21801  ismbf1  22638  ismbf  22642  mbfconst  22647  mbfres2  22657  cncombf  22670  isi1f  22688  itg1val  22697  deg1val  23101  fta1glem2  23173  fta1g  23174  fta1b  23176  dgrval  23238  dgrlem  23239  coeidlem  23247  coe11  23263  fta1lem  23316  fta1  23317  vieta1lem2  23320  vieta1  23321  taylthlem2  23385  areaval  23946  sqff1o  24165  nlfnval  27590  fimacnvinrn  28288  xppreima2  28302  ofpreima  28320  fpwrelmapffslem  28369  xrhval  28873  indf1ofs  28898  ismbfm  29124  mbfmcst  29131  issibf  29216  sitgfval  29224  eulerpartlemelr  29240  eulerpartleme  29246  eulerpartlemo  29248  eulerpartlemt0  29252  eulerpartlemt  29254  eulerpartlemr  29257  eulerpartlemgf  29262  eulerpartlemgs2  29263  eulerpartlemn  29264  eulerpart  29265  ballotlemscr  29401  ballotlemrv  29402  ballotlemrinv0  29415  ballotlemscrOLD  29439  ballotlemrvOLD  29440  ballotlemrinv0OLD  29453  iscvm  30032  cvmliftmolem1  30054  cvmlift2lem9a  30076  cvmlift2lem9  30084  msrfval  30225  ismfs  30237  mthmval  30263  poimirlem4  31990  poimirlem5  31991  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem10  31996  poimirlem11  31997  poimirlem12  31998  poimirlem13  31999  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem26  32012  poimirlem27  32013  poimirlem32  32018  cnambfre  32035  itg2addnclem2  32040  ftc1anclem1  32063  ftc1anclem6  32068  lkrval  32700  pw2f1o2val  35940  aomclem8  35965  pwfi2f1o  36000  trclimalb2  36364  frege131d  36402  dirkercncflem2  38067
  Copyright terms: Public domain W3C validator