Theorem imaeq1i 6056

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

Syntax hints:   = wceq 1541   “ cima 5679

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 2703

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 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by:  mptpreima  6237  csbpredg  6306  isarep2  6639  suppun  8171  suppco  8193  fsuppun  9384  fsuppcolem  9398  marypha2lem4  9435  dfoi  9508  r1limg  9768  isf34lem3  10372  compss  10373  fpwwe2lem12  10639  infrenegsup  12201  gsumzf1o  19821  ssidcn  22979  cnco  22990  qtopres  23422  idqtop  23430  qtopcn  23438  mbfid  25376  mbfres  25385  cncombf  25399  dvlog  26383  efopnlem2  26389  eucrct2eupth  29753  disjpreima  32070  imadifxp  32087  rinvf1o  32109  cyc3genpm  32569  mbfmcst  33544  mbfmco  33549  sitmcl  33636  eulerpartlemt  33656  eulerpartlemmf  33660  eulerpart  33667  0rrv  33736  mclsppslem  34860  bj-iminvid  36379  mptsnun  36523  poimirlem3  36794  ftc1anclem3  36866  areacirclem5  36883  cytpval  42253  arearect  42266  brtrclfv2  42780  0cnf  44892  fourierdlem62  45183  smfco  45817