Theorem imaeq1i 6013

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

Syntax hints:   = wceq 1541   “ cima 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  mptpreima  6193  csbpredg  6262  isarep2  6579  suppun  8123  suppco  8145  fsuppun  9282  fsuppcolem  9296  marypha2lem4  9333  dfoi  9408  r1limg  9675  isf34lem3  10277  compss  10278  fpwwe2lem12  10544  infrenegsup  12116  gsumzf1o  19832  ssidcn  23190  cnco  23201  qtopres  23633  idqtop  23641  qtopcn  23649  mbfid  25583  mbfres  25592  cncombf  25606  dvlog  26607  efopnlem2  26613  seqsval  28238  seqsfn  28259  seqsp1  28261  eucrct2eupth  30246  disjpreima  32585  imadifxp  32602  rinvf1o  32634  suppun2  32689  cyc3genpm  33162  elrgspnsubrunlem2  33258  esplysply  33657  vieta  33664  isconstr  33821  mbfmcst  34344  mbfmco  34349  sitmcl  34436  eulerpartlemt  34456  eulerpartlemmf  34460  eulerpart  34467  0rrv  34536  mclsppslem  35699  bj-iminvid  37312  mptsnun  37456  poimirlem3  37736  ftc1anclem3  37808  areacirclem5  37825  cytpval  43359  arearect  43372  brtrclfv2  43884  0cnf  46037  fourierdlem62  46328  smfco  46962