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

Theorem imaeq1i 6014
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 6012 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cima 5640
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-br 5110  df-opab 5172  df-cnv 5645  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650
This theorem is referenced by:  mptpreima  6194  csbpredg  6263  isarep2  6596  suppun  8119  suppco  8141  fsuppun  9332  fsuppcolem  9345  marypha2lem4  9382  dfoi  9455  r1limg  9715  isf34lem3  10319  compss  10320  fpwwe2lem12  10586  infrenegsup  12146  gsumzf1o  19697  ssidcn  22629  cnco  22640  qtopres  23072  idqtop  23080  qtopcn  23088  mbfid  25022  mbfres  25031  cncombf  25045  dvlog  26029  efopnlem2  26035  eucrct2eupth  29238  disjpreima  31555  imadifxp  31572  rinvf1o  31597  cyc3genpm  32057  mbfmcst  32923  mbfmco  32928  sitmcl  33015  eulerpartlemt  33035  eulerpartlemmf  33039  eulerpart  33046  0rrv  33115  mclsppslem  34241  bj-iminvid  35716  mptsnun  35860  poimirlem3  36131  ftc1anclem3  36203  areacirclem5  36220  cytpval  41583  arearect  41596  brtrclfv2  42091  0cnf  44208  fourierdlem62  44499  smfco  45133
  Copyright terms: Public domain W3C validator