Theorem imaeq1i 6049

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  mptpreima  6238  csbpredg  6309  isarep2  6627  suppun  8194  suppco  8216  fsuppun  9372  fsuppcolem  9386  marypha2lem4  9423  dfoi  9498  r1limg  9771  isf34lem3  10446  compss  10447  fpwwe2lem12  10720  infrenegsup  12293  gsumzf1o  20119  ssidcn  23566  cnco  23577  qtopres  24010  idqtop  24018  qtopcn  24026  mbfid  25949  mbfres  25958  cncombf  25972  dvlog  26972  efopnlem2  26978  seqsval  28667  seqsfn  28688  seqsp1  28690  eucrct2eupth  30839  disjpreima  33171  imadifxp  33188  rinvf1o  33217  suppun2  33270  cyc3genpm  33706  elrgspnsubrunlem2  33802  esplysply  34196  vieta  34205  isconstr  34361  mbfmcst  34884  mbfmco  34889  sitmcl  34976  eulerpartlemt  34996  eulerpartlemmf  35000  eulerpart  35007  0rrv  35076  mclsppslem  36327  bj-iminvid  38096  mptsnun  38242  poimirlem3  38521  ftc1anclem3  38593  areacirclem5  38610  cytpval  44188  arearect  44201  brtrclfv2  44712  0cnf  46856  fourierdlem62  47147  smfco  47781