Theorem imaeq1i 6067

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 6065	. 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-cnv 5666  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671

This theorem is used by:  mptpreima  6258  csbpredg  6336  isarep2  6659  suppun  8239  suppco  8261  fsuppun  9416  fsuppcolem  9430  marypha2lem4  9467  dfoi  9542  r1limg  9815  isf34lem3  10492  compss  10493  fpwwe2lem12  10766  infrenegsup  12340  gsumzf1o  20177  ssidcn  23628  cnco  23639  qtopres  24072  idqtop  24080  qtopcn  24088  mbfid  26011  mbfres  26020  cncombf  26034  dvlog  27036  efopnlem2  27042  seqsval  28731  seqsfn  28752  seqsp1  28754  eucrct2eupth  30903  disjpreima  33276  imadifxp  33293  rinvf1o  33322  suppun2  33374  cyc3genpm  33812  elrgspnsubrunlem2  33908  esplysply  34314  vieta  34323  isconstr  34479  mbfmcst  35002  mbfmco  35007  sitmcl  35094  eulerpartlemt  35114  eulerpartlemmf  35118  eulerpart  35125  0rrv  35194  mclsppslem  36556  bj-iminvid  38384  mptsnun  38530  poimirlem3  38809  ftc1anclem3  38881  areacirclem5  38898  cytpval  44465  arearect  44478  brtrclfv2  44988  0cnf  47160  fourierdlem62  47451  smfco  48085