Theorem imaeq2i 6023

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

Syntax hints:   = wceq 1542   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  cnvimarndm  6048  dmco  6219  imain  6583  fnimapr  6923  fnimatpd  6924  ssimaex  6925  intpreima  7022  resfunexg  7170  imauni  7201  isoini2  7294  fsuppeq  8125  fsuppeqg  8126  naddasslem1  8630  naddasslem2  8631  uniqs  8720  pwfilem  9228  fiint  9237  jech9.3  9738  infxpenlem  9935  hsmexlem4  10351  fcdmnn0supp  12494  fcdmnn0fsupp  12495  fcdmnn0suppg  12496  hashkf  14294  ghmeqker  19218  gsumval3lem1  19880  gsumval3lem2  19881  islinds2  21793  lindsind2  21799  mhpmulcl  22115  snclseqg  24081  retopbas  24725  ismbf3d  25621  i1fima  25645  i1fd  25648  itg1addlem5  25667  limciun  25861  plyeq0  26176  bday0  27803  bday1  27806  madeval2  27825  old1  27857  madeoldsuc  27877  bdayiun  27907  neg0s  28018  neg1s  28019  negbdaylem  28048  oncutlt  28256  oniso  28263  bdayons  28268  n0bday  28344  bdayn0p1  28361  spthispth  29792  0pth  30195  1pthdlem2  30206  eupth2lemb  30307  htth  30989  fcoinver  32674  ffs2  32800  ffsrn  32801  tocyccntz  33205  elrspunidl  33488  sibfof  34484  eulerpartgbij  34516  eulerpartlemmf  34519  eulerpartlemgh  34522  eulerpart  34526  fiblem  34542  orrvcval4  34609  cvmsss2  35456  opelco3  35957  poimirlem3  37944  poimirlem30  37971  mbfposadd  37988  itg2addnclem2  37993  ftc1anclem5  38018  ftc1anclem6  38019  pwfi2f1o  43524  brtrclfv2  44154  binomcxp  44784  fcoreslem1  47511  isubgr3stgrlem6  48447