Theorem imaeq2i 5929

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

Syntax hints:   = wceq 1537   “ cima 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  cnvimarndm  5952  dmco  6109  imain  6441  fnimapr  6749  ssimaex  6750  intpreima  6840  resfunexg  6980  imauni  7007  isoini2  7094  frnsuppeq  7844  imacosuppOLD  7877  uniqs  8359  fiint  8797  jech9.3  9245  infxpenlem  9441  hsmexlem4  9853  frnnn0supp  11956  hashkf  13695  ghmeqker  18387  gsumval3lem1  19027  gsumval3lem2  19028  islinds2  20959  lindsind2  20965  snclseqg  22726  retopbas  23371  ismbf3d  24257  i1fima  24281  i1fd  24284  itg1addlem5  24303  limciun  24494  plyeq0  24803  spthispth  27509  0pth  27906  1pthdlem2  27917  eupth2lemb  28018  htth  28697  fcoinver  30359  fnimatp  30425  ffs2  30466  ffsrn  30467  tocyccntz  30788  sibfof  31600  eulerpartgbij  31632  eulerpartlemmf  31635  eulerpartlemgh  31638  eulerpart  31642  fiblem  31658  orrvcval4  31724  cvmsss2  32523  opelco3  33020  madeval2  33292  poimirlem3  34897  poimirlem30  34924  mbfposadd  34941  itg2addnclem2  34946  ftc1anclem5  34973  ftc1anclem6  34974  uniqsALTV  35588  pwfi2f1o  39703  brtrclfv2  40079  binomcxp  40696