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 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

This proof depends on syntax axioms:   = wceq 1570   “ cima 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  mptpreima  6241  csbpredg  6312  isarep2  6629  suppun  8182  suppco  8204  fsuppun  9350  fsuppcolem  9364  marypha2lem4  9401  dfoi  9476  r1limg  9746  isf34lem3  10370  compss  10371  fpwwe2lem12  10638  infrenegsup  12209  gsumzf1o  20005  ssidcn  23441  cnco  23452  qtopres  23884  idqtop  23892  qtopcn  23900  mbfid  25823  mbfres  25832  cncombf  25846  dvlog  26845  efopnlem2  26851  seqsval  28510  seqsfn  28531  seqsp1  28533  eucrct2eupth  30625  disjpreima  32958  imadifxp  32975  rinvf1o  33004  suppun2  33058  cyc3genpm  33495  elrgspnsubrunlem2  33591  esplysply  33984  vieta  33993  isconstr  34149  mbfmcst  34673  mbfmco  34678  sitmcl  34765  eulerpartlemt  34785  eulerpartlemmf  34789  eulerpart  34796  0rrv  34865  mclsppslem  36088  bj-iminvid  37872  mptsnun  38018  poimirlem3  38307  ftc1anclem3  38379  areacirclem5  38396  cytpval  43962  arearect  43975  brtrclfv2  44486  0cnf  46624  fourierdlem62  46915  smfco  47549