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

Theorem imaeq1i 5902
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 5900 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  cima 5534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043  df-opab 5105  df-cnv 5539  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544
This theorem is referenced by:  mptpreima  6068  isarep2  6419  suppun  7828  suppco  7848  supp0cosupp0OLD  7851  imacosuppOLD  7853  fsuppun  8830  fsuppcolem  8842  marypha2lem4  8880  dfoi  8953  r1limg  9178  isf34lem3  9775  compss  9776  fpwwe2lem13  10042  infrenegsup  11602  gsumzf1o  19011  ssidcn  21839  cnco  21850  qtopres  22282  idqtop  22290  qtopcn  22298  mbfid  24218  mbfres  24227  cncombf  24241  dvlog  25221  efopnlem2  25227  eucrct2eupth  28009  disjpreima  30321  imadifxp  30338  rinvf1o  30362  cyc3genpm  30802  mbfmcst  31525  mbfmco  31530  sitmcl  31617  eulerpartlemt  31637  eulerpartlemmf  31641  eulerpart  31648  0rrv  31717  mclsppslem  32838  csbpredg  34624  mptsnun  34637  poimirlem3  34936  ftc1anclem3  35008  areacirclem5  35025  cytpval  39946  arearect  39958  brtrclfv2  40207  0cnf  42310  fourierdlem62  42601  smfco  43225
  Copyright terms: Public domain W3C validator