Theorem imaeq1i 6001

Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
imaeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
imaeq1i	⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

Proof of Theorem imaeq1i

Step	Hyp	Ref	Expression
1		imaeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		imaeq1 5999	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)

Syntax hints:   = wceq 1541   “ cima 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-cnv 5619  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624

This theorem is referenced by:  mptpreima  6180  csbpredg  6249  isarep2  6566  suppun  8109  suppco  8131  fsuppun  9266  fsuppcolem  9280  marypha2lem4  9317  dfoi  9392  r1limg  9659  isf34lem3  10261  compss  10262  fpwwe2lem12  10528  infrenegsup  12100  gsumzf1o  19819  ssidcn  23165  cnco  23176  qtopres  23608  idqtop  23616  qtopcn  23624  mbfid  25558  mbfres  25567  cncombf  25581  dvlog  26582  efopnlem2  26588  seqsval  28213  seqsfn  28234  seqsp1  28236  eucrct2eupth  30217  disjpreima  32556  imadifxp  32573  rinvf1o  32604  suppun2  32657  cyc3genpm  33113  elrgspnsubrunlem2  33207  esplysply  33584  isconstr  33741  mbfmcst  34264  mbfmco  34269  sitmcl  34356  eulerpartlemt  34376  eulerpartlemmf  34380  eulerpart  34387  0rrv  34456  mclsppslem  35619  bj-iminvid  37229  mptsnun  37373  poimirlem3  37663  ftc1anclem3  37735  areacirclem5  37752  cytpval  43235  arearect  43248  brtrclfv2  43760  0cnf  45915  fourierdlem62  46206  smfco  46840