Theorem imaeq1d 6051

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

Syntax hints:   → wi 4   = wceq 1563   “ cima 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is referenced by:  imaeq12d  6053  nfimad  6061  csbrn  6193  f1imacnv  6827  foimacnv  6828  fimacnvinrn  7056  seqomeq12  8429  ssenen  9127  fipreima  9303  oieq1  9462  oieq2  9463  dfac12lem1  10115  dfac12r  10118  fpwwe2cbv  10603  fpwwe2lem2  10605  fpwwecbv  10617  fpwwelem  10618  seqeq1  14028  seqeq2  14029  seqeq3  14030  1arith  16975  vdwmc  17026  vdwnnlem1  17043  ramub2  17062  rami  17063  imasless  17582  gsumvalx  18722  eqglact  19235  eqg0subgecsn  19256  psgnunilem1  19551  evpmss  21693  psgnevpmb  21694  frlmup3  21907  psrbag  22024  psrbaglefi  22033  iscn  23349  ptbasfi  23695  ptval2  23715  ptrescn  23753  xkoptsub  23768  qtopval  23809  cmphaushmeo  23914  ptcmpg  24171  restutopopn  24352  prdsxmslem2  24643  metuval  24663  nghmfval  24836  isnghm  24837  ismbf1  25740  ismbf  25744  mbfconst  25749  mbfres2  25761  cncombf  25774  isi1f  25790  itg1val  25799  deg1val  26210  fta1glem2  26283  fta1g  26284  fta1b  26286  dgrval  26342  dgrlem  26343  coeidlem  26351  coe11  26367  fta1lem  26425  fta1  26426  vieta1lem2  26429  vieta1  26430  taylthlem2  26491  areaval  27083  sqff1o  27300  seqseq123d  28433  nlfnval  32138  xppreima2  32904  ofpreima  32918  mptiffisupp  32946  fpwrelmapffslem  32985  indf1ofs  33094  evpmval  33373  altgnsg  33377  ply1dg3rt0irred  33786  vieta  33882  xrhval  34320  ismbfm  34553  mbfmcst  34561  issibf  34635  sitgfval  34643  eulerpartlemelr  34659  eulerpartleme  34665  eulerpartlemo  34667  eulerpartlemt0  34671  eulerpartlemt  34673  eulerpartlemr  34676  eulerpartlemgf  34681  eulerpartlemgs2  34682  eulerpartlemn  34683  eulerpart  34684  ballotlemscr  34821  ballotlemrv  34822  ballotlemrinv0  34835  iscvm  35617  cvmliftmolem1  35639  cvmlift2lem9a  35661  cvmlift2lem9  35669  msrfval  35895  ismfs  35907  mthmval  35933  ttcid  36860  bj-imdirval2  37682  bj-iminvval2  37693  poimirlem4  38130  poimirlem5  38131  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem10  38136  poimirlem11  38137  poimirlem12  38138  poimirlem13  38139  poimirlem14  38140  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem18  38144  poimirlem19  38145  poimirlem20  38146  poimirlem21  38147  poimirlem22  38148  poimirlem26  38152  poimirlem27  38153  poimirlem32  38158  cnambfre  38174  itg2addnclem2  38178  ftc1anclem1  38199  ftc1anclem6  38204  lkrval  39719  aks6d1c6lem4  42797  aks6d1c6lem5  42801  aks6d1c7lem3  42806  prjcrvfval  43220  prjcrvval  43221  prjcrv0  43222  pw2f1o2val  43623  aomclem8  43645  pwfi2f1o  43680  trclimalb2  44309  frege131d  44347  colleq12d  44822  dirkercncflem2  46677  issmflem  47300  smfpimioo  47360  smfpimcc  47381  smfsuplem2  47385  3f1oss1  47668  imaidfu2lem  49739  imaidfu  49740  imaidfu2  49741