Theorem imaeq1i 6016

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

Syntax hints:   = wceq 1547   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  mptpreima  6196  csbpredg  6265  isarep2  6582  suppun  8131  suppco  8153  fsuppun  9297  fsuppcolem  9311  marypha2lem4  9348  dfoi  9423  r1limg  9693  isf34lem3  10295  compss  10296  fpwwe2lem12  10563  infrenegsup  12137  gsumzf1o  19885  ssidcn  23245  cnco  23256  qtopres  23688  idqtop  23696  qtopcn  23704  mbfid  25627  mbfres  25636  cncombf  25650  dvlog  26640  efopnlem2  26646  seqsval  28305  seqsfn  28326  seqsp1  28328  eucrct2eupth  30340  disjpreima  32680  imadifxp  32697  rinvf1o  32729  suppun2  32783  cyc3genpm  33240  elrgspnsubrunlem2  33336  esplysply  33762  vieta  33771  isconstr  33927  mbfmcst  34450  mbfmco  34455  sitmcl  34542  eulerpartlemt  34562  eulerpartlemmf  34566  eulerpart  34573  0rrv  34642  mclsppslem  35818  bj-iminvid  37562  mptsnun  37708  poimirlem3  37997  ftc1anclem3  38069  areacirclem5  38086  cytpval  43654  arearect  43667  brtrclfv2  44178  0cnf  46327  fourierdlem62  46618  smfco  47252