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 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   “ cima 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  imaeq12d  6053  nfimad  6065  csbrn  6203  f1imacnv  6839  foimacnv  6840  fimacnvinrn  7069  seqomeq12  8457  ssenen  9163  fipreima  9340  oieq1  9499  oieq2  9500  dfac12lem1  10215  dfac12r  10218  fpwwe2cbv  10708  fpwwe2lem2  10710  fpwwecbv  10722  fpwwelem  10723  seqeq1  14140  seqeq2  14141  seqeq3  14142  1arith  17098  vdwmc  17149  vdwnnlem1  17166  ramub2  17185  rami  17186  imasless  17705  gsumvalx  18858  eqglact  19384  eqg0subgecsn  19405  psgnunilem1  19700  evpmss  21885  psgnevpmb  21886  frlmup3  22099  psrbag  22218  psrbaglefi  22227  iscn  23546  ptbasfi  23893  ptval2  23913  ptrescn  23951  xkoptsub  23966  qtopval  24007  cmphaushmeo  24112  ptcmpg  24369  restutopopn  24550  prdsxmslem2  24841  metuval  24861  nghmfval  25034  isnghm  25035  ismbf1  25938  ismbf  25942  mbfconst  25947  mbfres2  25959  cncombf  25972  isi1f  25988  itg1val  25997  deg1val  26407  fta1glem2  26480  fta1g  26481  fta1b  26483  dgrval  26540  dgrlem  26541  coeidlem  26549  coe11  26565  fta1lem  26621  fta1  26622  vieta1lem2  26627  vieta1  26628  taylthlem2  26694  areaval  27285  sqff1o  27502  seqseq123d  28665  nlfnval  32476  xppreima2  33238  ofpreima  33252  mptiffisupp  33279  fpwrelmapffslem  33317  indf1ofs  33426  evpmval  33699  altgnsg  33703  ply1dg3rt0irred  34109  vieta  34205  xrhval  34643  ismbfm  34877  mbfmcst  34884  issibf  34958  sitgfval  34966  eulerpartlemelr  34982  eulerpartleme  34988  eulerpartlemo  34990  eulerpartlemt0  34994  eulerpartlemt  34996  eulerpartlemr  34999  eulerpartlemgf  35004  eulerpartlemgs2  35005  eulerpartlemn  35006  eulerpart  35007  ballotlemscr  35144  ballotlemrv  35145  ballotlemrinv0  35158  iscvm  36003  cvmliftmolem1  36025  cvmlift2lem9a  36047  cvmlift2lem9  36055  msrfval  36281  ismfs  36293  mthmval  36319  ttcid  37260  bj-imdirval2  38084  bj-iminvval2  38095  poimirlem4  38522  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem26  38544  poimirlem27  38545  poimirlem32  38550  cnambfre  38566  itg2addnclem2  38570  ftc1anclem1  38591  ftc1anclem6  38596  lkrval  40125  aks6d1c6lem4  43203  aks6d1c6lem5  43207  aks6d1c7lem3  43212  prjcrvfval  43647  prjcrvval  43648  prjcrv0  43649  pw2f1o2val  44025  aomclem8  44047  pwfi2f1o  44082  trclimalb2  44711  frege131d  44749  colleq12d  45222  dirkercncflem2  47083  issmflem  47706  smfpimioo  47766  smfpimcc  47787  smfsuplem2  47791  3f1oss1  48114  imaidfu2lem  50186  imaidfu  50187  imaidfu2  50188