Theorem imaeq1d 6043

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 6039	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1559   “ cima 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656

This theorem is referenced by:  imaeq12d  6045  nfimad  6053  csbrn  6184  f1imacnv  6817  foimacnv  6818  fimacnvinrn  7046  seqomeq12  8418  ssenen  9116  fipreima  9294  oieq1  9453  oieq2  9454  dfac12lem1  10093  dfac12r  10096  fpwwe2cbv  10581  fpwwe2lem2  10583  fpwwecbv  10595  fpwwelem  10596  seqeq1  14010  seqeq2  14011  seqeq3  14012  1arith  16953  vdwmc  17004  vdwnnlem1  17021  ramub2  17040  rami  17041  imasless  17560  gsumvalx  18700  eqglact  19210  eqg0subgecsn  19228  psgnunilem1  19523  evpmss  21625  psgnevpmb  21626  frlmup3  21839  psrbag  21956  psrbaglefi  21965  iscn  23282  ptbasfi  23628  ptval2  23648  ptrescn  23686  xkoptsub  23701  qtopval  23742  cmphaushmeo  23847  ptcmpg  24104  restutopopn  24285  prdsxmslem2  24576  metuval  24596  nghmfval  24769  isnghm  24770  ismbf1  25673  ismbf  25677  mbfconst  25682  mbfres2  25694  cncombf  25707  isi1f  25723  itg1val  25732  deg1val  26143  fta1glem2  26216  fta1g  26217  fta1b  26219  dgrval  26275  dgrlem  26276  coeidlem  26284  coe11  26300  fta1lem  26358  fta1  26359  vieta1lem2  26362  vieta1  26363  taylthlem2  26424  areaval  27016  sqff1o  27233  seqseq123d  28366  nlfnval  32040  xppreima2  32813  ofpreima  32827  mptiffisupp  32855  fpwrelmapffslem  32894  indf1ofs  33004  evpmval  33285  altgnsg  33289  ply1dg3rt0irred  33740  vieta  33837  xrhval  34275  ismbfm  34508  mbfmcst  34516  issibf  34590  sitgfval  34598  eulerpartlemelr  34614  eulerpartleme  34620  eulerpartlemo  34622  eulerpartlemt0  34626  eulerpartlemt  34628  eulerpartlemr  34631  eulerpartlemgf  34636  eulerpartlemgs2  34637  eulerpartlemn  34638  eulerpart  34639  ballotlemscr  34776  ballotlemrv  34777  ballotlemrinv0  34790  iscvm  35569  cvmliftmolem1  35591  cvmlift2lem9a  35613  cvmlift2lem9  35621  msrfval  35847  ismfs  35859  mthmval  35885  ttcid  36812  bj-imdirval2  37635  bj-iminvval2  37646  poimirlem4  38083  poimirlem5  38084  poimirlem6  38085  poimirlem7  38086  poimirlem8  38087  poimirlem10  38089  poimirlem11  38090  poimirlem12  38091  poimirlem13  38092  poimirlem14  38093  poimirlem15  38094  poimirlem16  38095  poimirlem17  38096  poimirlem18  38097  poimirlem19  38098  poimirlem20  38099  poimirlem21  38100  poimirlem22  38101  poimirlem26  38105  poimirlem27  38106  poimirlem32  38111  cnambfre  38127  itg2addnclem2  38131  ftc1anclem1  38152  ftc1anclem6  38157  lkrval  39672  aks6d1c6lem4  42750  aks6d1c6lem5  42754  aks6d1c7lem3  42759  prjcrvfval  43173  prjcrvval  43174  prjcrv0  43175  pw2f1o2val  43576  aomclem8  43598  pwfi2f1o  43633  trclimalb2  44262  frege131d  44300  colleq12d  44789  dirkercncflem2  46638  issmflem  47261  smfpimioo  47321  smfpimcc  47342  smfsuplem2  47346  3f1oss1  47629  imaidfu2lem  49690  imaidfu  49691  imaidfu2  49692