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

Theorem imaeq1i 5619
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 5617 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  cima 5267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-br 4803  df-opab 4863  df-cnv 5272  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277
This theorem is referenced by:  mptpreima  5787  isarep2  6137  suppun  7481  supp0cosupp0  7501  imacosupp  7502  fsuppun  8457  fsuppcolem  8469  marypha2lem4  8507  dfoi  8579  r1limg  8805  isf34lem3  9387  compss  9388  fpwwe2lem13  9654  infrenegsup  11196  gsumzf1o  18511  ssidcn  21259  cnco  21270  qtopres  21701  idqtop  21709  qtopcn  21717  mbfid  23600  mbfres  23608  cncombf  23622  dvlog  24594  efopnlem2  24600  eucrct2eupth  27395  disjpreima  29702  imadifxp  29719  rinvf1o  29739  mbfmcst  30628  mbfmco  30633  sitmcl  30720  eulerpartlemt  30740  eulerpartlemmf  30744  eulerpart  30751  0rrv  30820  mclsppslem  31785  csbpredg  33481  mptsnun  33495  poimirlem3  33723  ftc1anclem3  33798  areacirclem5  33815  cytpval  38287  arearect  38301  brtrclfv2  38519  0cnf  40591  mbf0  40674  fourierdlem62  40886  smfco  41513
  Copyright terms: Public domain W3C validator