Theorem imaeq1d 6024

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

Syntax hints:   → wi 4   = wceq 1542   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaeq12d  6026  nfimad  6034  csbrn  6167  f1imacnv  6796  foimacnv  6797  fimacnvinrn  7023  seqomeq12  8393  ssenen  9089  fipreima  9268  oieq1  9427  oieq2  9428  dfac12lem1  10066  dfac12r  10069  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwecbv  10567  fpwwelem  10568  seqeq1  13966  seqeq2  13967  seqeq3  13968  1arith  16898  vdwmc  16949  vdwnnlem1  16966  ramub2  16985  rami  16986  imasless  17504  gsumvalx  18644  eqglact  19154  eqg0subgecsn  19172  psgnunilem1  19468  evpmss  21566  psgnevpmb  21567  frlmup3  21780  psrbag  21897  psrbaglefi  21906  iscn  23200  ptbasfi  23546  ptval2  23566  ptrescn  23604  xkoptsub  23619  qtopval  23660  cmphaushmeo  23765  ptcmpg  24022  restutopopn  24203  prdsxmslem2  24494  metuval  24514  nghmfval  24687  isnghm  24688  ismbf1  25591  ismbf  25595  mbfconst  25600  mbfres2  25612  cncombf  25625  isi1f  25641  itg1val  25650  deg1val  26061  fta1glem2  26134  fta1g  26135  fta1b  26137  dgrval  26193  dgrlem  26194  coeidlem  26202  coe11  26218  fta1lem  26273  fta1  26274  vieta1lem2  26277  vieta1  26278  taylthlem2  26339  areaval  26928  sqff1o  27145  seqseq123d  28278  nlfnval  31952  xppreima2  32724  ofpreima  32738  mptiffisupp  32766  fpwrelmapffslem  32805  indf1ofs  32926  evpmval  33206  altgnsg  33210  ply1dg3rt0irred  33644  vieta  33724  xrhval  34162  ismbfm  34395  mbfmcst  34403  issibf  34477  sitgfval  34485  eulerpartlemelr  34501  eulerpartleme  34507  eulerpartlemo  34509  eulerpartlemt0  34513  eulerpartlemt  34515  eulerpartlemr  34518  eulerpartlemgf  34523  eulerpartlemgs2  34524  eulerpartlemn  34525  eulerpart  34526  ballotlemscr  34663  ballotlemrv  34664  ballotlemrinv0  34677  iscvm  35441  cvmliftmolem1  35463  cvmlift2lem9a  35485  cvmlift2lem9  35493  msrfval  35719  ismfs  35731  mthmval  35757  ttcid  36674  bj-imdirval2  37497  bj-iminvval2  37508  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem26  37967  poimirlem27  37968  poimirlem32  37973  cnambfre  37989  itg2addnclem2  37993  ftc1anclem1  38014  ftc1anclem6  38019  lkrval  39534  aks6d1c6lem4  42612  aks6d1c6lem5  42616  aks6d1c7lem3  42621  prjcrvfval  43064  prjcrvval  43065  prjcrv0  43066  pw2f1o2val  43467  aomclem8  43489  pwfi2f1o  43524  trclimalb2  44153  frege131d  44191  colleq12d  44680  dirkercncflem2  46532  issmflem  47155  smfpimioo  47215  smfpimcc  47236  smfsuplem2  47240  3f1oss1  47523  imaidfu2lem  49584  imaidfu  49585  imaidfu2  49586