Theorem imaeq1i 6053

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  mptpreima  6234  csbpredg  6305  isarep2  6622  suppun  8182  suppco  8204  fsuppun  9357  fsuppcolem  9371  marypha2lem4  9408  dfoi  9483  r1limg  9753  isf34lem3  10377  compss  10378  fpwwe2lem12  10651  infrenegsup  12222  gsumzf1o  20039  ssidcn  23480  cnco  23491  qtopres  23924  idqtop  23932  qtopcn  23940  mbfid  25863  mbfres  25872  cncombf  25886  dvlog  26888  efopnlem2  26894  seqsval  28553  seqsfn  28574  seqsp1  28576  eucrct2eupth  30725  disjpreima  33057  imadifxp  33074  rinvf1o  33103  suppun2  33156  cyc3genpm  33592  elrgspnsubrunlem2  33688  esplysply  34081  vieta  34090  isconstr  34246  mbfmcst  34770  mbfmco  34775  sitmcl  34862  eulerpartlemt  34882  eulerpartlemmf  34886  eulerpart  34893  0rrv  34962  mclsppslem  36162  bj-iminvid  37947  mptsnun  38093  poimirlem3  38372  ftc1anclem3  38444  areacirclem5  38461  cytpval  44043  arearect  44056  brtrclfv2  44567  0cnf  46705  fourierdlem62  46996  smfco  47630