Theorem imaeq2i 6010

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

Syntax hints:   = wceq 1547   “ cima 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631

This theorem is referenced by:  cnvimarndm  6035  dmco  6206  imain  6570  fnimapr  6910  fnimatpd  6911  ssimaex  6912  intpreima  7011  resfunexg  7159  imauni  7190  isoini2  7283  fsuppeq  8115  fsuppeqg  8116  naddasslem1  8620  naddasslem2  8621  uniqs  8710  pwfilem  9218  fiint  9227  jech9.3  9729  infxpenlem  9926  hsmexlem4  10342  fcdmnn0supp  12485  fcdmnn0fsupp  12486  fcdmnn0suppg  12487  hashkf  14285  ghmeqker  19209  gsumval3lem1  19871  gsumval3lem2  19872  islinds2  21788  lindsind2  21794  mhpmulcl  22137  snclseqg  24099  retopbas  24743  ismbf3d  25639  i1fima  25663  i1fd  25666  itg1addlem5  25685  limciun  25879  plyeq0  26194  bday0  27821  bday1  27824  madeval2  27843  old1  27875  madeoldsuc  27895  bdayiun  27925  neg0s  28036  neg1s  28037  negbdaylem  28066  oncutlt  28274  oniso  28281  bdayons  28286  n0bday  28362  bdayn0p1  28379  spthispth  29810  0pth  30213  1pthdlem2  30224  eupth2lemb  30325  htth  31007  fcoinver  32693  ffs2  32819  ffsrn  32820  tocyccntz  33225  elrspunidl  33511  sibfof  34524  eulerpartgbij  34556  eulerpartlemmf  34559  eulerpartlemgh  34562  eulerpart  34566  fiblem  34582  orrvcval4  34649  cvmsss2  35502  opelco3  36003  poimirlem3  37990  poimirlem30  38017  mbfposadd  38034  itg2addnclem2  38039  ftc1anclem5  38064  ftc1anclem6  38065  pwfi2f1o  43541  brtrclfv2  44171  binomcxp  44801  fcoreslem1  47526  isubgr3stgrlem6  48462