Theorem imaeq1d 5971

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

Syntax hints:   → wi 4   = wceq 1539   “ cima 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603

This theorem is referenced by:  imaeq12d  5973  nfimad  5981  csbrn  6111  f1imacnv  6741  foimacnv  6742  fimacnvinrn  6958  seqomeq12  8294  ssenen  8947  fipreima  9134  oieq1  9280  oieq2  9281  dfac12lem1  9908  dfac12r  9911  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwecbv  10409  fpwwelem  10410  seqeq1  13733  seqeq2  13734  seqeq3  13735  1arith  16637  vdwmc  16688  vdwnnlem1  16705  ramub2  16724  rami  16725  imasless  17260  gsumvalx  18369  eqglact  18816  psgnunilem1  19110  evpmss  20800  psgnevpmb  20801  frlmup3  21016  psrbag  21129  psrbaglefi  21144  psrbaglefiOLD  21145  iscn  22395  ptbasfi  22741  ptval2  22761  ptrescn  22799  xkoptsub  22814  qtopval  22855  cmphaushmeo  22960  ptcmpg  23217  restutopopn  23399  prdsxmslem2  23694  metuval  23714  nghmfval  23895  isnghm  23896  ismbf1  24797  ismbf  24801  mbfconst  24806  mbfres2  24818  cncombf  24831  isi1f  24847  itg1val  24856  deg1val  25270  fta1glem2  25340  fta1g  25341  fta1b  25343  dgrval  25398  dgrlem  25399  coeidlem  25407  coe11  25423  fta1lem  25476  fta1  25477  vieta1lem2  25480  vieta1  25481  taylthlem2  25542  areaval  26123  sqff1o  26340  nlfnval  30252  xppreima2  30997  ofpreima  31011  fpwrelmapffslem  31076  evpmval  31421  altgnsg  31425  xrhval  31977  indf1ofs  32003  ismbfm  32228  mbfmcst  32235  issibf  32309  sitgfval  32317  eulerpartlemelr  32333  eulerpartleme  32339  eulerpartlemo  32341  eulerpartlemt0  32345  eulerpartlemt  32347  eulerpartlemr  32350  eulerpartlemgf  32355  eulerpartlemgs2  32356  eulerpartlemn  32357  eulerpart  32358  ballotlemscr  32494  ballotlemrv  32495  ballotlemrinv0  32508  iscvm  33230  cvmliftmolem1  33252  cvmlift2lem9a  33274  cvmlift2lem9  33282  msrfval  33508  ismfs  33520  mthmval  33546  bj-imdirval2  35363  bj-iminvval2  35374  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem26  35812  poimirlem27  35813  poimirlem32  35818  cnambfre  35834  itg2addnclem2  35838  ftc1anclem1  35859  ftc1anclem6  35864  lkrval  37109  prjcrvfval  40475  prjcrvval  40476  prjcrv0  40477  pw2f1o2val  40868  aomclem8  40893  pwfi2f1o  40928  trclimalb2  41341  frege131d  41379  colleq12d  41878  dirkercncflem2  43652  issmflem  44272  smfpimioo  44332  smfpimcc  44352  smfsuplem2  44356