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

Theorem imaeq1i 5919
Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
Hypothesis
Ref Expression
imaeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
imaeq1i (𝐴𝐶) = (𝐵𝐶)

Proof of Theorem imaeq1i
StepHypRef Expression
1 imaeq1i.1 . 2 𝐴 = 𝐵
2 imaeq1 5917 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  cima 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561
This theorem is referenced by:  mptpreima  6085  isarep2  6436  suppun  7839  suppco  7859  supp0cosupp0OLD  7862  imacosuppOLD  7864  fsuppun  8840  fsuppcolem  8852  marypha2lem4  8890  dfoi  8963  r1limg  9188  isf34lem3  9785  compss  9786  fpwwe2lem13  10052  infrenegsup  11612  gsumzf1o  18961  ssidcn  21791  cnco  21802  qtopres  22234  idqtop  22242  qtopcn  22250  mbfid  24163  mbfres  24172  cncombf  24186  dvlog  25161  efopnlem2  25167  eucrct2eupth  27951  disjpreima  30262  imadifxp  30279  rinvf1o  30303  cyc3genpm  30721  mbfmcst  31416  mbfmco  31421  sitmcl  31508  eulerpartlemt  31528  eulerpartlemmf  31532  eulerpart  31539  0rrv  31608  mclsppslem  32727  csbpredg  34489  mptsnun  34502  poimirlem3  34776  ftc1anclem3  34850  areacirclem5  34867  cytpval  39687  arearect  39700  brtrclfv2  39950  0cnf  42036  fourierdlem62  42330  smfco  42954
  Copyright terms: Public domain W3C validator