Theorem imaeq1i 6028

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

Syntax hints:   = wceq 1540   “ cima 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  mptpreima  6211  csbpredg  6280  isarep2  6608  suppun  8163  suppco  8185  fsuppun  9338  fsuppcolem  9352  marypha2lem4  9389  dfoi  9464  r1limg  9724  isf34lem3  10328  compss  10329  fpwwe2lem12  10595  infrenegsup  12166  gsumzf1o  19842  ssidcn  23142  cnco  23153  qtopres  23585  idqtop  23593  qtopcn  23601  mbfid  25536  mbfres  25545  cncombf  25559  dvlog  26560  efopnlem2  26566  seqsval  28182  seqsfn  28203  seqsp1  28205  eucrct2eupth  30174  disjpreima  32513  imadifxp  32530  rinvf1o  32554  suppun2  32607  cyc3genpm  33109  elrgspnsubrunlem2  33199  isconstr  33726  mbfmcst  34250  mbfmco  34255  sitmcl  34342  eulerpartlemt  34362  eulerpartlemmf  34366  eulerpart  34373  0rrv  34442  mclsppslem  35570  bj-iminvid  37183  mptsnun  37327  poimirlem3  37617  ftc1anclem3  37689  areacirclem5  37706  cytpval  43191  arearect  43204  brtrclfv2  43716  0cnf  45875  fourierdlem62  46166  smfco  46800