Theorem imaeq1i 6048

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

This proof depends on syntax axioms:   = wceq 1569   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  mptpreima  6239  csbpredg  6310  isarep2  6630  suppun  8205  suppco  8227  fsuppun  9383  fsuppcolem  9397  marypha2lem4  9434  dfoi  9509  r1limg  9782  isf34lem3  10457  compss  10458  fpwwe2lem12  10731  infrenegsup  12304  gsumzf1o  20132  ssidcn  23579  cnco  23590  qtopres  24023  idqtop  24031  qtopcn  24039  mbfid  25962  mbfres  25971  cncombf  25985  dvlog  26985  efopnlem2  26991  seqsval  28680  seqsfn  28701  seqsp1  28703  eucrct2eupth  30852  disjpreima  33226  imadifxp  33243  rinvf1o  33272  suppun2  33325  cyc3genpm  33760  elrgspnsubrunlem2  33856  esplysply  34250  vieta  34259  isconstr  34415  mbfmcst  34938  mbfmco  34943  sitmcl  35030  eulerpartlemt  35050  eulerpartlemmf  35054  eulerpart  35061  0rrv  35130  mclsppslem  36435  bj-iminvid  38210  mptsnun  38356  poimirlem3  38635  ftc1anclem3  38707  areacirclem5  38724  cytpval  44298  arearect  44311  brtrclfv2  44821  0cnf  46981  fourierdlem62  47272  smfco  47906