Theorem imaeq1d 6014

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  imaeq12d  6016  nfimad  6024  csbrn  6156  f1imacnv  6784  foimacnv  6785  fimacnvinrn  7009  seqomeq12  8383  ssenen  9075  fipreima  9267  oieq1  9423  oieq2  9424  dfac12lem1  10057  dfac12r  10060  fpwwe2cbv  10543  fpwwe2lem2  10545  fpwwecbv  10557  fpwwelem  10558  seqeq1  13929  seqeq2  13930  seqeq3  13931  1arith  16857  vdwmc  16908  vdwnnlem1  16925  ramub2  16944  rami  16945  imasless  17462  gsumvalx  18568  eqglact  19076  eqg0subgecsn  19094  psgnunilem1  19390  evpmss  21511  psgnevpmb  21512  frlmup3  21725  psrbag  21842  psrbaglefi  21851  iscn  23138  ptbasfi  23484  ptval2  23504  ptrescn  23542  xkoptsub  23557  qtopval  23598  cmphaushmeo  23703  ptcmpg  23960  restutopopn  24142  prdsxmslem2  24433  metuval  24453  nghmfval  24626  isnghm  24627  ismbf1  25541  ismbf  25545  mbfconst  25550  mbfres2  25562  cncombf  25575  isi1f  25591  itg1val  25600  deg1val  26017  fta1glem2  26090  fta1g  26091  fta1b  26093  dgrval  26149  dgrlem  26150  coeidlem  26158  coe11  26174  fta1lem  26231  fta1  26232  vieta1lem2  26235  vieta1  26236  taylthlem2  26298  taylthlem2OLD  26299  areaval  26890  sqff1o  27108  seqseq123d  28203  nlfnval  31843  xppreima2  32608  ofpreima  32622  mptiffisupp  32649  fpwrelmapffslem  32688  indf1ofs  32822  evpmval  33100  altgnsg  33104  ply1dg3rt0irred  33530  xrhval  33987  ismbfm  34220  mbfmcst  34229  issibf  34303  sitgfval  34311  eulerpartlemelr  34327  eulerpartleme  34333  eulerpartlemo  34335  eulerpartlemt0  34339  eulerpartlemt  34341  eulerpartlemr  34344  eulerpartlemgf  34349  eulerpartlemgs2  34350  eulerpartlemn  34351  eulerpart  34352  ballotlemscr  34489  ballotlemrv  34490  ballotlemrinv0  34503  iscvm  35234  cvmliftmolem1  35256  cvmlift2lem9a  35278  cvmlift2lem9  35286  msrfval  35512  ismfs  35524  mthmval  35550  bj-imdirval2  37159  bj-iminvval2  37170  poimirlem4  37606  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem13  37615  poimirlem14  37616  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem26  37628  poimirlem27  37629  poimirlem32  37634  cnambfre  37650  itg2addnclem2  37654  ftc1anclem1  37675  ftc1anclem6  37680  lkrval  39069  aks6d1c6lem4  42149  aks6d1c6lem5  42153  aks6d1c7lem3  42158  prjcrvfval  42607  prjcrvval  42608  prjcrv0  42609  pw2f1o2val  43015  aomclem8  43037  pwfi2f1o  43072  trclimalb2  43702  frege131d  43740  colleq12d  44229  dirkercncflem2  46089  issmflem  46712  smfpimioo  46772  smfpimcc  46793  smfsuplem2  46797  3f1oss1  47063  imaidfu2lem  49098  imaidfu  49099  imaidfu2  49100