Theorem imaeq2i 5804

Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
imaeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
imaeq2i	⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)

Proof of Theorem imaeq2i

Step	Hyp	Ref	Expression
1		imaeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		imaeq2 5802	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)

Syntax hints:   = wceq 1522   “ cima 5446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-br 4963  df-opab 5025  df-xp 5449  df-cnv 5451  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456

This theorem is referenced by:  cnvimarndm  5826  dmco  5982  imain  6309  fnimapr  6614  ssimaex  6615  intpreima  6703  resfunexg  6844  imauni  6870  isoini2  6955  frnsuppeq  7693  imacosuppOLD  7726  uniqs  8207  fiint  8641  jech9.3  9089  infxpenlem  9285  hsmexlem4  9697  frnnn0supp  11801  hashkf  13542  ghmeqker  18126  gsumval3lem1  18746  gsumval3lem2  18747  islinds2  20639  lindsind2  20645  snclseqg  22407  retopbas  23052  ismbf3d  23938  i1fima  23962  i1fd  23965  itg1addlem5  23984  limciun  24175  plyeq0  24484  spthispth  27194  0pth  27591  1pthdlem2  27602  eupth2lemb  27704  htth  28386  fcoinver  30047  fnimatp  30113  ffs2  30152  ffsrn  30153  tocyccntz  30423  sibfof  31215  eulerpartgbij  31247  eulerpartlemmf  31250  eulerpartlemgh  31253  eulerpart  31257  fiblem  31273  orrvcval4  31339  cvmsss2  32130  opelco3  32627  madeval2  32900  poimirlem3  34445  poimirlem30  34472  mbfposadd  34489  itg2addnclem2  34494  ftc1anclem5  34521  ftc1anclem6  34522  uniqsALTV  35137  pwfi2f1o  39200  brtrclfv2  39576  binomcxp  40246