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

Step	Hyp	Ref	Expression
1		imaeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		imaeq1 5892	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

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