Theorem imaeq1i 6015

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

Syntax hints:   = wceq 1541   “ cima 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  mptpreima  6195  csbpredg  6264  isarep2  6597  suppun  8120  suppco  8142  fsuppun  9333  fsuppcolem  9346  marypha2lem4  9383  dfoi  9456  r1limg  9716  isf34lem3  10320  compss  10321  fpwwe2lem12  10587  infrenegsup  12147  gsumzf1o  19703  ssidcn  22643  cnco  22654  qtopres  23086  idqtop  23094  qtopcn  23102  mbfid  25036  mbfres  25045  cncombf  25059  dvlog  26043  efopnlem2  26049  eucrct2eupth  29252  disjpreima  31569  imadifxp  31586  rinvf1o  31611  cyc3genpm  32071  mbfmcst  32948  mbfmco  32953  sitmcl  33040  eulerpartlemt  33060  eulerpartlemmf  33064  eulerpart  33071  0rrv  33140  mclsppslem  34264  bj-iminvid  35739  mptsnun  35883  poimirlem3  36154  ftc1anclem3  36226  areacirclem5  36243  cytpval  41594  arearect  41607  brtrclfv2  42121  0cnf  44238  fourierdlem62  44529  smfco  45163