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

Theorem imaeq1i 5894
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 5892 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cima 5522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3399  df-un 3846  df-in 3848  df-ss 3858  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028  df-opab 5090  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532
This theorem is referenced by:  mptpreima  6064  isarep2  6422  suppun  7872  suppco  7894  fsuppun  8918  fsuppcolem  8931  marypha2lem4  8968  dfoi  9041  r1limg  9266  isf34lem3  9868  compss  9869  fpwwe2lem12  10135  infrenegsup  11694  gsumzf1o  19144  ssidcn  21999  cnco  22010  qtopres  22442  idqtop  22450  qtopcn  22458  mbfid  24380  mbfres  24389  cncombf  24403  dvlog  25386  efopnlem2  25392  eucrct2eupth  28174  disjpreima  30489  imadifxp  30506  rinvf1o  30531  cyc3genpm  30988  mbfmcst  31788  mbfmco  31793  sitmcl  31880  eulerpartlemt  31900  eulerpartlemmf  31904  eulerpart  31911  0rrv  31980  mclsppslem  33108  bj-iminvid  34976  csbpredg  35109  mptsnun  35122  poimirlem3  35392  ftc1anclem3  35464  areacirclem5  35481  cytpval  40590  arearect  40602  brtrclfv2  40865  0cnf  42944  fourierdlem62  43235  smfco  43859
  Copyright terms: Public domain W3C validator