Theorem imaeq1i 5382

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

Syntax hints:   = wceq 1475   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  mptpreima  5545  isarep2  5892  suppun  7202  supp0cosupp0  7221  imacosupp  7222  fsuppun  8177  fsuppcolem  8189  marypha2lem4  8227  dfoi  8299  r1limg  8517  isf34lem3  9080  compss  9081  fpwwe2lem13  9343  infrenegsup  10883  gsumzf1o  18136  ssidcn  20869  cnco  20880  qtopres  21311  idqtop  21319  qtopcn  21327  mbfid  23209  mbfres  23217  cncombf  23231  dvlog  24197  efopnlem2  24203  disjpreima  28779  imadifxp  28796  rinvf1o  28814  mbfmcst  29648  mbfmco  29653  sitmcl  29740  eulerpartlemt  29760  eulerpartlemmf  29764  eulerpart  29771  0rrv  29840  mclsppslem  30734  csbpredg  32348  mptsnun  32362  poimirlem3  32582  ftc1anclem3  32657  areacirclem5  32674  cytpval  36806  arearect  36820  brtrclfv2  37038  0cnf  38762  mbf0  38849  fourierdlem62  39061  smfco  39687  eucrct2eupth  41413