Theorem imaeq2i 6068

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

This proof depends on syntax axioms:   = wceq 1570   “ cima 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671

This theorem is used by:  cnvimarndmOLD  6099  dmco  6275  imain  6655  fnimapr  6999  fnimatpd  7000  ssimaex  7001  intpreima  7102  resfunexg  7252  imauni  7281  isoini2  7378  fsuppeq  8230  fsuppeqg  8231  naddasslem1  8742  naddasslem2  8743  uniqs  8832  pwfilem  9347  fiint  9356  jech9.3OLD  9860  infxpenlem  10131  hsmexlem4  10546  fcdmnn0supp  12703  fcdmnn0fsupp  12704  fcdmnn0suppg  12705  hashkf  14517  ghmeqker  19507  gsumval3lem1  20170  gsumval3lem2  20171  islinds2  22174  lindsind2  22180  mhpmulcl  22525  snclseqg  24490  retopbas  25134  ismbf3d  26030  i1fima  26054  i1fd  26057  itg1addlem5  26076  limciun  26269  plyeq0  26585  rnplynfin  26685  bday0  28254  bday1  28257  madeval2  28276  old1  28308  madeoldsuc  28328  bdayiun  28358  neg0s  28469  neg1s  28470  negbdaylem  28499  oncutlt  28707  oniso  28714  bdayons  28719  n0bday  28795  bdayn0p1  28812  spthispth  30366  0pth  30773  1pthdlem2  30784  eupth2lemb  30895  htth  31577  fcoinver  33296  ffs2  33415  ffsrn  33416  tocyccntz  33804  elrspunidl  34082  sibfof  35083  eulerpartgbij  35115  eulerpartlemmf  35118  eulerpartlemgh  35121  eulerpart  35125  fiblem  35141  orrvcval4  35208  cvmsss2  36247  opelco3  36754  poimirlem3  38809  poimirlem30  38836  mbfposadd  38853  itg2addnclem2  38858  ftc1anclem5  38883  ftc1anclem6  38884  pwfi2f1o  44364  brtrclfv2  44988  binomcxp  45602  fcoreslem1  48406  isubgr3stgrlem6  49342