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

Theorem imaeq1i 5969
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 5967 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  cima 5593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603
This theorem is referenced by:  mptpreima  6146  csbpredg  6212  isarep2  6532  suppun  8009  suppco  8031  fsuppun  9156  fsuppcolem  9169  marypha2lem4  9206  dfoi  9279  r1limg  9538  isf34lem3  10140  compss  10141  fpwwe2lem12  10407  infrenegsup  11967  gsumzf1o  19522  ssidcn  22415  cnco  22426  qtopres  22858  idqtop  22866  qtopcn  22874  mbfid  24808  mbfres  24817  cncombf  24831  dvlog  25815  efopnlem2  25821  eucrct2eupth  28618  disjpreima  30932  imadifxp  30949  rinvf1o  30974  cyc3genpm  31428  mbfmcst  32235  mbfmco  32240  sitmcl  32327  eulerpartlemt  32347  eulerpartlemmf  32351  eulerpart  32358  0rrv  32427  mclsppslem  33554  bj-iminvid  35375  mptsnun  35519  poimirlem3  35789  ftc1anclem3  35861  areacirclem5  35878  cytpval  41041  arearect  41053  brtrclfv2  41342  0cnf  43425  fourierdlem62  43716  smfco  44347
  Copyright terms: Public domain W3C validator