Theorem imaeq1d 6050

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  imaeq12d  6052  nfimad  6064  csbrn  6204  f1imacnv  6842  foimacnv  6843  fimacnvinrn  7072  seqomeq12  8468  ssenen  9174  fipreima  9351  oieq1  9510  oieq2  9511  dfac12lem1  10226  dfac12r  10229  fpwwe2cbv  10719  fpwwe2lem2  10721  fpwwecbv  10733  fpwwelem  10734  seqeq1  14151  seqeq2  14152  seqeq3  14153  1arith  17111  vdwmc  17162  vdwnnlem1  17179  ramub2  17198  rami  17199  imasless  17718  gsumvalx  18871  eqglact  19397  eqg0subgecsn  19418  psgnunilem1  19713  evpmss  21898  psgnevpmb  21899  frlmup3  22112  psrbag  22231  psrbaglefi  22240  iscn  23559  ptbasfi  23906  ptval2  23926  ptrescn  23964  xkoptsub  23979  qtopval  24020  cmphaushmeo  24125  ptcmpg  24382  restutopopn  24563  prdsxmslem2  24854  metuval  24874  nghmfval  25047  isnghm  25048  ismbf1  25951  ismbf  25955  mbfconst  25960  mbfres2  25972  cncombf  25985  isi1f  26001  itg1val  26010  deg1val  26420  fta1glem2  26493  fta1g  26494  fta1b  26496  dgrval  26553  dgrlem  26554  coeidlem  26562  coe11  26578  fta1lem  26634  fta1  26635  vieta1lem2  26640  vieta1  26641  taylthlem2  26707  areaval  27298  sqff1o  27515  seqseq123d  28678  nlfnval  32489  xppreima2  33293  ofpreima  33307  mptiffisupp  33334  fpwrelmapffslem  33371  indf1ofs  33480  evpmval  33753  altgnsg  33757  ply1dg3rt0irred  34163  vieta  34259  xrhval  34697  ismbfm  34931  mbfmcst  34938  issibf  35012  sitgfval  35020  eulerpartlemelr  35036  eulerpartleme  35042  eulerpartlemo  35044  eulerpartlemt0  35048  eulerpartlemt  35050  eulerpartlemr  35053  eulerpartlemgf  35058  eulerpartlemgs2  35059  eulerpartlemn  35060  eulerpart  35061  ballotlemscr  35198  ballotlemrv  35199  ballotlemrinv0  35212  iscvm  36111  cvmliftmolem1  36133  cvmlift2lem9a  36155  cvmlift2lem9  36163  msrfval  36389  ismfs  36401  mthmval  36427  ttcid  37373  bj-imdirval2  38198  bj-iminvval2  38209  poimirlem4  38636  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem8  38640  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem13  38645  poimirlem14  38646  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem18  38650  poimirlem19  38651  poimirlem20  38652  poimirlem21  38653  poimirlem22  38654  poimirlem26  38658  poimirlem27  38659  poimirlem32  38664  cnambfre  38680  itg2addnclem2  38684  ftc1anclem1  38705  ftc1anclem6  38710  lkrval  40239  aks6d1c6lem4  43317  aks6d1c6lem5  43321  aks6d1c7lem3  43326  prjcrvfval  43761  prjcrvval  43762  prjcrv0  43763  pw2f1o2val  44140  aomclem8  44157  pwfi2f1o  44192  trclimalb2  44820  frege131d  44858  colleq12d  45331  dirkercncflem2  47208  issmflem  47831  smfpimioo  47891  smfpimcc  47912  smfsuplem2  47916  3f1oss1  48239  imaidfu2lem  50319  imaidfu  50320  imaidfu2  50321