Theorem imaeq1i 6061

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

Syntax hints:   = wceq 1570   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  mptpreima  6241  csbpredg  6310  isarep2  6627  suppun  8181  suppco  8203  fsuppun  9348  fsuppcolem  9362  marypha2lem4  9399  dfoi  9474  r1limg  9744  isf34lem3  10360  compss  10361  fpwwe2lem12  10628  infrenegsup  12199  gsumzf1o  19983  ssidcn  23393  cnco  23404  qtopres  23836  idqtop  23844  qtopcn  23852  mbfid  25775  mbfres  25784  cncombf  25798  dvlog  26797  efopnlem2  26803  seqsval  28462  seqsfn  28483  seqsp1  28485  eucrct2eupth  30577  disjpreima  32910  imadifxp  32927  rinvf1o  32956  suppun2  33010  cyc3genpm  33453  elrgspnsubrunlem2  33549  esplysply  33942  vieta  33951  isconstr  34107  mbfmcst  34630  mbfmco  34635  sitmcl  34722  eulerpartlemt  34742  eulerpartlemmf  34746  eulerpart  34753  0rrv  34822  mclsppslem  36056  bj-iminvid  37820  mptsnun  37966  poimirlem3  38255  ftc1anclem3  38327  areacirclem5  38344  cytpval  43912  arearect  43925  brtrclfv2  44436  0cnf  46574  fourierdlem62  46865  smfco  47499