Theorem imaeq2i 6047

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

Syntax hints:   = wceq 1560   “ cima 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660

This theorem is referenced by:  cnvimarndm  6072  dmco  6242  imain  6606  fnimapr  6950  fnimatpd  6951  ssimaex  6952  intpreima  7051  resfunexg  7199  imauni  7230  isoini2  7323  fsuppeq  8155  fsuppeqg  8156  naddasslem1  8665  naddasslem2  8666  uniqs  8755  pwfilem  9262  fiint  9271  jech9.3  9772  infxpenlem  9969  hsmexlem4  10386  fcdmnn0supp  12538  fcdmnn0fsupp  12539  fcdmnn0suppg  12540  hashkf  14345  ghmeqker  19283  gsumval3lem1  19945  gsumval3lem2  19946  islinds2  21862  lindsind2  21868  mhpmulcl  22211  snclseqg  24173  retopbas  24817  ismbf3d  25713  i1fima  25737  i1fd  25740  itg1addlem5  25759  limciun  25953  plyeq0  26268  bday0  27901  bday1  27904  madeval2  27923  old1  27955  madeoldsuc  27975  bdayiun  28005  neg0s  28116  neg1s  28117  negbdaylem  28146  oncutlt  28354  oniso  28361  bdayons  28366  n0bday  28442  bdayn0p1  28459  spthispth  29921  0pth  30324  1pthdlem2  30335  eupth2lemb  30436  htth  31118  fcoinver  32801  ffs2  32926  ffsrn  32927  tocyccntz  33321  elrspunidl  33611  sibfof  34634  eulerpartgbij  34666  eulerpartlemmf  34669  eulerpartlemgh  34672  eulerpart  34676  fiblem  34692  orrvcval4  34759  cvmsss2  35621  opelco3  36122  poimirlem3  38119  poimirlem30  38146  mbfposadd  38163  itg2addnclem2  38168  ftc1anclem5  38193  ftc1anclem6  38194  pwfi2f1o  43670  brtrclfv2  44300  binomcxp  44930  fcoreslem1  47654  isubgr3stgrlem6  48590