Theorem imaeq1d 6079

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

Syntax hints:   → wi 4   = wceq 1537   “ cima 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702

This theorem is referenced by:  imaeq12d  6081  nfimad  6089  csbrn  6225  f1imacnv  6865  foimacnv  6866  fimacnvinrn  7091  seqomeq12  8493  ssenen  9190  fipreima  9396  oieq1  9550  oieq2  9551  dfac12lem1  10182  dfac12r  10185  fpwwe2cbv  10668  fpwwe2lem2  10670  fpwwecbv  10682  fpwwelem  10683  seqeq1  14042  seqeq2  14043  seqeq3  14044  1arith  16961  vdwmc  17012  vdwnnlem1  17029  ramub2  17048  rami  17049  imasless  17587  gsumvalx  18702  eqglact  19210  eqg0subgecsn  19228  psgnunilem1  19526  evpmss  21622  psgnevpmb  21623  frlmup3  21838  psrbag  21955  psrbaglefi  21964  iscn  23259  ptbasfi  23605  ptval2  23625  ptrescn  23663  xkoptsub  23678  qtopval  23719  cmphaushmeo  23824  ptcmpg  24081  restutopopn  24263  prdsxmslem2  24558  metuval  24578  nghmfval  24759  isnghm  24760  ismbf1  25673  ismbf  25677  mbfconst  25682  mbfres2  25694  cncombf  25707  isi1f  25723  itg1val  25732  deg1val  26150  fta1glem2  26223  fta1g  26224  fta1b  26226  dgrval  26282  dgrlem  26283  coeidlem  26291  coe11  26307  fta1lem  26364  fta1  26365  vieta1lem2  26368  vieta1  26369  taylthlem2  26431  taylthlem2OLD  26432  areaval  27022  sqff1o  27240  seqseq123d  28307  nlfnval  31910  xppreima2  32668  ofpreima  32682  mptiffisupp  32708  fpwrelmapffslem  32750  evpmval  33148  altgnsg  33152  ply1dg3rt0irred  33587  xrhval  33981  indf1ofs  34007  ismbfm  34232  mbfmcst  34241  issibf  34315  sitgfval  34323  eulerpartlemelr  34339  eulerpartleme  34345  eulerpartlemo  34347  eulerpartlemt0  34351  eulerpartlemt  34353  eulerpartlemr  34356  eulerpartlemgf  34361  eulerpartlemgs2  34362  eulerpartlemn  34363  eulerpart  34364  ballotlemscr  34500  ballotlemrv  34501  ballotlemrinv0  34514  iscvm  35244  cvmliftmolem1  35266  cvmlift2lem9a  35288  cvmlift2lem9  35296  msrfval  35522  ismfs  35534  mthmval  35560  bj-imdirval2  37166  bj-iminvval2  37177  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem26  37633  poimirlem27  37634  poimirlem32  37639  cnambfre  37655  itg2addnclem2  37659  ftc1anclem1  37680  ftc1anclem6  37685  lkrval  39070  aks6d1c6lem4  42155  aks6d1c6lem5  42159  aks6d1c7lem3  42164  prjcrvfval  42618  prjcrvval  42619  prjcrv0  42620  pw2f1o2val  43028  aomclem8  43050  pwfi2f1o  43085  trclimalb2  43716  frege131d  43754  colleq12d  44249  dirkercncflem2  46060  issmflem  46683  smfpimioo  46743  smfpimcc  46764  smfsuplem2  46768  3f1oss1  47025