Theorem imaeq1d 6051

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
imaeq1d	⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Proof of Theorem imaeq1d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		imaeq1 6047	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1540   “ cima 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  imaeq12d  6053  nfimad  6061  csbrn  6197  f1imacnv  6839  foimacnv  6840  fimacnvinrn  7066  seqomeq12  8473  ssenen  9170  fipreima  9375  oieq1  9531  oieq2  9532  dfac12lem1  10163  dfac12r  10166  fpwwe2cbv  10649  fpwwe2lem2  10651  fpwwecbv  10663  fpwwelem  10664  seqeq1  14027  seqeq2  14028  seqeq3  14029  1arith  16952  vdwmc  17003  vdwnnlem1  17020  ramub2  17039  rami  17040  imasless  17559  gsumvalx  18659  eqglact  19167  eqg0subgecsn  19185  psgnunilem1  19479  evpmss  21551  psgnevpmb  21552  frlmup3  21765  psrbag  21882  psrbaglefi  21891  iscn  23178  ptbasfi  23524  ptval2  23544  ptrescn  23582  xkoptsub  23597  qtopval  23638  cmphaushmeo  23743  ptcmpg  24000  restutopopn  24182  prdsxmslem2  24473  metuval  24493  nghmfval  24666  isnghm  24667  ismbf1  25582  ismbf  25586  mbfconst  25591  mbfres2  25603  cncombf  25616  isi1f  25632  itg1val  25641  deg1val  26058  fta1glem2  26131  fta1g  26132  fta1b  26134  dgrval  26190  dgrlem  26191  coeidlem  26199  coe11  26215  fta1lem  26272  fta1  26273  vieta1lem2  26276  vieta1  26277  taylthlem2  26339  taylthlem2OLD  26340  areaval  26931  sqff1o  27149  seqseq123d  28237  nlfnval  31867  xppreima2  32634  ofpreima  32648  mptiffisupp  32675  fpwrelmapffslem  32714  indf1ofs  32848  evpmval  33161  altgnsg  33165  ply1dg3rt0irred  33600  xrhval  34054  ismbfm  34287  mbfmcst  34296  issibf  34370  sitgfval  34378  eulerpartlemelr  34394  eulerpartleme  34400  eulerpartlemo  34402  eulerpartlemt0  34406  eulerpartlemt  34408  eulerpartlemr  34411  eulerpartlemgf  34416  eulerpartlemgs2  34417  eulerpartlemn  34418  eulerpart  34419  ballotlemscr  34556  ballotlemrv  34557  ballotlemrinv0  34570  iscvm  35286  cvmliftmolem1  35308  cvmlift2lem9a  35330  cvmlift2lem9  35338  msrfval  35564  ismfs  35576  mthmval  35602  bj-imdirval2  37206  bj-iminvval2  37217  poimirlem4  37653  poimirlem5  37654  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem10  37659  poimirlem11  37660  poimirlem12  37661  poimirlem13  37662  poimirlem14  37663  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem18  37667  poimirlem19  37668  poimirlem20  37669  poimirlem21  37670  poimirlem22  37671  poimirlem26  37675  poimirlem27  37676  poimirlem32  37681  cnambfre  37697  itg2addnclem2  37701  ftc1anclem1  37722  ftc1anclem6  37727  lkrval  39111  aks6d1c6lem4  42191  aks6d1c6lem5  42195  aks6d1c7lem3  42200  prjcrvfval  42629  prjcrvval  42630  prjcrv0  42631  pw2f1o2val  43038  aomclem8  43060  pwfi2f1o  43095  trclimalb2  43725  frege131d  43763  colleq12d  44252  dirkercncflem2  46113  issmflem  46736  smfpimioo  46796  smfpimcc  46817  smfsuplem2  46821  3f1oss1  47084  imaidfu2lem  49048  imaidfu  49049  imaidfu2  49050