Theorem imaeq2i 5464

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

Syntax hints:   = wceq 1483   “ cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  cnvimarndm  5486  dmco  5643  imain  5974  fnimapr  6262  ssimaex  6263  intpreima  6346  resfunexg  6479  imauni  6504  isoini2  6589  frnsuppeq  7307  imacosupp  7335  uniqs  7807  fiint  8237  jech9.3  8677  infxpenlem  8836  hsmexlem4  9251  frnnn0supp  11349  hashkf  13119  ghmeqker  17687  gsumval3lem1  18306  gsumval3lem2  18307  islinds2  20152  lindsind2  20158  snclseqg  21919  retopbas  22564  ismbf3d  23421  i1fima  23445  i1fd  23448  itg1addlem5  23467  limciun  23658  plyeq0  23967  spthispth  26622  0pth  26986  1pthdlem2  26996  eupth2lemb  27097  htth  27775  fcoinver  29418  ffs2  29503  ffsrn  29504  sibfof  30402  eulerpartgbij  30434  eulerpartlemmf  30437  eulerpartlemgh  30440  eulerpart  30444  fiblem  30460  orrvcval4  30526  cvmsss2  31256  opelco3  31678  madeval2  31936  poimirlem3  33412  poimirlem30  33439  mbfposadd  33457  itg2addnclem2  33462  ftc1anclem5  33489  ftc1anclem6  33490  uniqsALTV  34101  pwfi2f1o  37666  brtrclfv2  38019  binomcxp  38556