Theorem imaeq1d 6057

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

Syntax hints:   → wi 4   = wceq 1534   “ cima 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144  df-opab 5206  df-cnv 5681  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686

This theorem is referenced by:  imaeq12d  6059  nfimad  6067  csbrn  6202  f1imacnv  6850  foimacnv  6851  fimacnvinrn  7076  seqomeq12  8469  ssenen  9170  fipreima  9377  oieq1  9530  oieq2  9531  dfac12lem1  10161  dfac12r  10164  fpwwe2cbv  10648  fpwwe2lem2  10650  fpwwecbv  10662  fpwwelem  10663  seqeq1  13996  seqeq2  13997  seqeq3  13998  1arith  16890  vdwmc  16941  vdwnnlem1  16958  ramub2  16977  rami  16978  imasless  17516  gsumvalx  18630  eqglact  19128  eqg0subgecsn  19146  psgnunilem1  19442  evpmss  21512  psgnevpmb  21513  frlmup3  21728  psrbag  21844  psrbaglefi  21859  psrbaglefiOLD  21860  iscn  23133  ptbasfi  23479  ptval2  23499  ptrescn  23537  xkoptsub  23552  qtopval  23593  cmphaushmeo  23698  ptcmpg  23955  restutopopn  24137  prdsxmslem2  24432  metuval  24452  nghmfval  24633  isnghm  24634  ismbf1  25547  ismbf  25551  mbfconst  25556  mbfres2  25568  cncombf  25581  isi1f  25597  itg1val  25606  deg1val  26026  fta1glem2  26097  fta1g  26098  fta1b  26100  dgrval  26156  dgrlem  26157  coeidlem  26165  coe11  26181  fta1lem  26236  fta1  26237  vieta1lem2  26240  vieta1  26241  taylthlem2  26303  taylthlem2OLD  26304  areaval  26890  sqff1o  27108  seqseq123d  28153  nlfnval  31685  xppreima2  32431  ofpreima  32445  mptiffisupp  32468  fpwrelmapffslem  32509  evpmval  32861  altgnsg  32865  xrhval  33614  indf1ofs  33640  ismbfm  33865  mbfmcst  33874  issibf  33948  sitgfval  33956  eulerpartlemelr  33972  eulerpartleme  33978  eulerpartlemo  33980  eulerpartlemt0  33984  eulerpartlemt  33986  eulerpartlemr  33989  eulerpartlemgf  33994  eulerpartlemgs2  33995  eulerpartlemn  33996  eulerpart  33997  ballotlemscr  34133  ballotlemrv  34134  ballotlemrinv0  34147  iscvm  34864  cvmliftmolem1  34886  cvmlift2lem9a  34908  cvmlift2lem9  34916  msrfval  35142  ismfs  35154  mthmval  35180  bj-imdirval2  36657  bj-iminvval2  36668  poimirlem4  37092  poimirlem5  37093  poimirlem6  37094  poimirlem7  37095  poimirlem8  37096  poimirlem10  37098  poimirlem11  37099  poimirlem12  37100  poimirlem13  37101  poimirlem14  37102  poimirlem15  37103  poimirlem16  37104  poimirlem17  37105  poimirlem18  37106  poimirlem19  37107  poimirlem20  37108  poimirlem21  37109  poimirlem22  37110  poimirlem26  37114  poimirlem27  37115  poimirlem32  37120  cnambfre  37136  itg2addnclem2  37140  ftc1anclem1  37161  ftc1anclem6  37166  lkrval  38555  aks6d1c6lem4  41640  aks6d1c6lem5  41644  prjcrvfval  42046  prjcrvval  42047  prjcrv0  42048  pw2f1o2val  42451  aomclem8  42476  pwfi2f1o  42511  trclimalb2  43147  frege131d  43185  colleq12d  43681  dirkercncflem2  45483  issmflem  46106  smfpimioo  46166  smfpimcc  46187  smfsuplem2  46191