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

Theorem imaeq1i 5183
Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
Hypothesis
Ref Expression
imaeq1i.1  |-  A  =  B
Assertion
Ref Expression
imaeq1i  |-  ( A
" C )  =  ( B " C
)

Proof of Theorem imaeq1i
StepHypRef Expression
1 imaeq1i.1 . 2  |-  A  =  B
2 imaeq1 5181 . 2  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
31, 2ax-mp 5 1  |-  ( A
" C )  =  ( B " C
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454   "cima 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-cnv 4860  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865
This theorem is referenced by:  mptpreima  5346  isarep2  5684  suppun  6961  supp0cosupp0  6980  imacosupp  6981  fsuppun  7927  fsuppcolem  7939  marypha2lem4  7977  dfoi  8051  r1limg  8267  isf34lem3  8830  compss  8831  fpwwe2lem13  9092  infrenegsup  10618  infmsupOLD  10619  gsumzf1o  17594  ssidcn  20319  cnco  20330  qtopres  20761  idqtop  20769  qtopcn  20777  mbfid  22640  mbfres  22648  cncombf  22662  dvlog  23644  efopnlem2  23650  disjpreima  28242  imadifxp  28260  rinvf1o  28278  mbfmcst  29129  mbfmco  29134  sitmcl  29232  eulerpartlemt  29252  eulerpartlemmf  29256  eulerpart  29263  0rrv  29332  mclsppslem  30269  csbpredg  31771  mptsnun  31785  poimirlem3  31987  ftc1anclem3  32063  areacirclem5  32080  cytpval  36130  arearect  36144  brtrclfv2  36363  0cnf  37791  mbf0  37871  fourierdlem62  38069
  Copyright terms: Public domain W3C validator