Theorem imaeq1i 6086

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

Syntax hints:   = wceq 1537   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  mptpreima  6269  csbpredg  6338  isarep2  6669  suppun  8225  suppco  8247  fsuppun  9456  fsuppcolem  9470  marypha2lem4  9507  dfoi  9580  r1limg  9840  isf34lem3  10444  compss  10445  fpwwe2lem12  10711  infrenegsup  12278  gsumzf1o  19954  ssidcn  23284  cnco  23295  qtopres  23727  idqtop  23735  qtopcn  23743  mbfid  25689  mbfres  25698  cncombf  25712  dvlog  26711  efopnlem2  26717  seqsval  28312  seqsfn  28333  seqsp1  28335  eucrct2eupth  30277  disjpreima  32606  imadifxp  32623  rinvf1o  32649  cyc3genpm  33145  mbfmcst  34224  mbfmco  34229  sitmcl  34316  eulerpartlemt  34336  eulerpartlemmf  34340  eulerpart  34347  0rrv  34416  mclsppslem  35551  bj-iminvid  37161  mptsnun  37305  poimirlem3  37583  ftc1anclem3  37655  areacirclem5  37672  cytpval  43163  arearect  43176  brtrclfv2  43689  0cnf  45798  fourierdlem62  46089  smfco  46723