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

Theorem imaeq1i 5267
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 5265 . 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 1370   "cima 4944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-br 4394  df-opab 4452  df-cnv 4949  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954
This theorem is referenced by:  mptpreima  5432  isarep2  5599  suppun  6812  supp0cosupp0  6831  imacosupp  6832  fsuppun  7743  fsuppcolem  7754  marypha2lem4  7792  dfoi  7829  mapfienOLD  8031  r1limg  8082  isf34lem3  8648  compss  8649  fpwwe2lem13  8913  infmsup  10412  gsumval3OLD  16495  gsumzf1o  16504  gsumzf1oOLD  16507  gsumzaddlemOLD  16523  dprdfidOLD  16628  funsnfsupOLD  17786  ssidcn  18984  cnco  18995  qtopres  19396  idqtop  19404  qtopcn  19412  mbfid  21240  mbfres  21248  cncombf  21262  dvlog  22222  efopnlem2  22228  disjpreima  26072  imadifxp  26083  rinvf1o  26093  mbfmcst  26811  mbfmco  26816  eulerpartlemt  26891  eulerpartlemmf  26895  eulerpart  26902  0rrv  26971  ftc1anclem3  28610  areacirclem5  28629  cytpval  29718  arearect  29732
  Copyright terms: Public domain W3C validator