Theorem imaeq1i 5969

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

Syntax hints:   = wceq 1539   “ cima 5593

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603

This theorem is referenced by:  mptpreima  6146  csbpredg  6212  isarep2  6532  suppun  8009  suppco  8031  fsuppun  9156  fsuppcolem  9169  marypha2lem4  9206  dfoi  9279  r1limg  9538  isf34lem3  10140  compss  10141  fpwwe2lem12  10407  infrenegsup  11967  gsumzf1o  19522  ssidcn  22415  cnco  22426  qtopres  22858  idqtop  22866  qtopcn  22874  mbfid  24808  mbfres  24817  cncombf  24831  dvlog  25815  efopnlem2  25821  eucrct2eupth  28618  disjpreima  30932  imadifxp  30949  rinvf1o  30974  cyc3genpm  31428  mbfmcst  32235  mbfmco  32240  sitmcl  32327  eulerpartlemt  32347  eulerpartlemmf  32351  eulerpart  32358  0rrv  32427  mclsppslem  33554  bj-iminvid  35375  mptsnun  35519  poimirlem3  35789  ftc1anclem3  35861  areacirclem5  35878  cytpval  41041  arearect  41053  brtrclfv2  41342  0cnf  43425  fourierdlem62  43716  smfco  44347