Theorem imaeq1i 6016

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

Syntax hints:   = wceq 1542   “ cima 5627

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  mptpreima  6196  csbpredg  6265  isarep2  6582  suppun  8127  suppco  8149  fsuppun  9293  fsuppcolem  9307  marypha2lem4  9344  dfoi  9419  r1limg  9686  isf34lem3  10288  compss  10289  fpwwe2lem12  10556  infrenegsup  12130  gsumzf1o  19878  ssidcn  23230  cnco  23241  qtopres  23673  idqtop  23681  qtopcn  23689  mbfid  25612  mbfres  25621  cncombf  25635  dvlog  26628  efopnlem2  26634  seqsval  28294  seqsfn  28315  seqsp1  28317  eucrct2eupth  30330  disjpreima  32669  imadifxp  32686  rinvf1o  32718  suppun2  32772  cyc3genpm  33228  elrgspnsubrunlem2  33324  esplysply  33730  vieta  33739  isconstr  33896  mbfmcst  34419  mbfmco  34424  sitmcl  34511  eulerpartlemt  34531  eulerpartlemmf  34535  eulerpart  34542  0rrv  34611  mclsppslem  35781  bj-iminvid  37525  mptsnun  37669  poimirlem3  37958  ftc1anclem3  38030  areacirclem5  38047  cytpval  43648  arearect  43661  brtrclfv2  44172  0cnf  46323  fourierdlem62  46614  smfco  47248