Theorem imaeq1i 5893

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 5891	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

Syntax hints:   = wceq 1538   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  mptpreima  6059  isarep2  6413  suppun  7833  suppco  7853  supp0cosupp0OLD  7856  imacosuppOLD  7858  fsuppun  8836  fsuppcolem  8848  marypha2lem4  8886  dfoi  8959  r1limg  9184  isf34lem3  9786  compss  9787  fpwwe2lem13  10053  infrenegsup  11611  gsumzf1o  19025  ssidcn  21860  cnco  21871  qtopres  22303  idqtop  22311  qtopcn  22319  mbfid  24239  mbfres  24248  cncombf  24262  dvlog  25242  efopnlem2  25248  eucrct2eupth  28030  disjpreima  30347  imadifxp  30364  rinvf1o  30389  cyc3genpm  30844  mbfmcst  31627  mbfmco  31632  sitmcl  31719  eulerpartlemt  31739  eulerpartlemmf  31743  eulerpart  31750  0rrv  31819  mclsppslem  32943  bj-iminvid  34610  csbpredg  34743  mptsnun  34756  poimirlem3  35060  ftc1anclem3  35132  areacirclem5  35149  cytpval  40153  arearect  40165  brtrclfv2  40428  0cnf  42519  fourierdlem62  42810  smfco  43434