Theorem imaeq1i 6022

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

Syntax hints:   = wceq 1542   “ cima 5634

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  mptpreima  6202  csbpredg  6271  isarep2  6588  suppun  8134  suppco  8156  fsuppun  9300  fsuppcolem  9314  marypha2lem4  9351  dfoi  9426  r1limg  9695  isf34lem3  10297  compss  10298  fpwwe2lem12  10565  infrenegsup  12139  gsumzf1o  19887  ssidcn  23220  cnco  23231  qtopres  23663  idqtop  23671  qtopcn  23679  mbfid  25602  mbfres  25611  cncombf  25625  dvlog  26615  efopnlem2  26621  seqsval  28280  seqsfn  28301  seqsp1  28303  eucrct2eupth  30315  disjpreima  32654  imadifxp  32671  rinvf1o  32703  suppun2  32757  cyc3genpm  33213  elrgspnsubrunlem2  33309  esplysply  33715  vieta  33724  isconstr  33880  mbfmcst  34403  mbfmco  34408  sitmcl  34495  eulerpartlemt  34515  eulerpartlemmf  34519  eulerpart  34526  0rrv  34595  mclsppslem  35765  bj-iminvid  37509  mptsnun  37655  poimirlem3  37944  ftc1anclem3  38016  areacirclem5  38033  cytpval  43630  arearect  43643  brtrclfv2  44154  0cnf  46305  fourierdlem62  46596  smfco  47230