Theorem imaeq2i 6055

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

This proof depends on syntax axioms:   = wceq 1569   “ cima 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-xp 5660  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667

This theorem is used by:  cnvimarndmOLD  6086  dmco  6262  imain  6633  fnimapr  6976  fnimatpd  6977  ssimaex  6978  intpreima  7078  resfunexg  7228  imauni  7257  isoini2  7354  fsuppeq  8203  fsuppeqg  8204  naddasslem1  8715  naddasslem2  8716  uniqs  8805  pwfilem  9320  fiint  9329  jech9.3OLD  9833  infxpenlem  10102  hsmexlem4  10517  fcdmnn0supp  12673  fcdmnn0fsupp  12674  fcdmnn0suppg  12675  hashkf  14486  ghmeqker  19469  gsumval3lem1  20131  gsumval3lem2  20132  islinds2  22131  lindsind2  22137  mhpmulcl  22482  snclseqg  24447  retopbas  25091  ismbf3d  25987  i1fima  26011  i1fd  26014  itg1addlem5  26033  limciun  26226  plyeq0  26542  rnplynfin  26642  bday0  28209  bday1  28212  madeval2  28231  old1  28263  madeoldsuc  28283  bdayiun  28313  neg0s  28424  neg1s  28425  negbdaylem  28454  oncutlt  28662  oniso  28669  bdayons  28674  n0bday  28750  bdayn0p1  28767  spthispth  30321  0pth  30728  1pthdlem2  30739  eupth2lemb  30850  htth  31532  fcoinver  33252  ffs2  33372  ffsrn  33373  tocyccntz  33758  elrspunidl  34031  sibfof  35025  eulerpartgbij  35057  eulerpartlemmf  35060  eulerpartlemgh  35063  eulerpart  35067  fiblem  35083  orrvcval4  35150  cvmsss2  36160  opelco3  36666  poimirlem3  38681  poimirlem30  38708  mbfposadd  38725  itg2addnclem2  38730  ftc1anclem5  38755  ftc1anclem6  38756  pwfi2f1o  44238  brtrclfv2  44867  binomcxp  45481  fcoreslem1  48272  isubgr3stgrlem6  49208