Theorem imaeq1d 6060

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-cnv 5668  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673

This theorem is used by:  imaeq12d  6062  nfimad  6070  csbrn  6203  f1imacnv  6837  foimacnv  6838  fimacnvinrn  7066  seqomeq12  8439  ssenen  9137  fipreima  9313  oieq1  9472  oieq2  9473  dfac12lem1  10134  dfac12r  10137  fpwwe2cbv  10621  fpwwe2lem2  10623  fpwwecbv  10635  fpwwelem  10636  seqeq1  14047  seqeq2  14048  seqeq3  14049  1arith  16993  vdwmc  17044  vdwnnlem1  17061  ramub2  17080  rami  17081  imasless  17600  gsumvalx  18740  eqglact  19253  eqg0subgecsn  19274  psgnunilem1  19569  evpmss  21747  psgnevpmb  21748  frlmup3  21961  psrbag  22078  psrbaglefi  22087  iscn  23403  ptbasfi  23749  ptval2  23769  ptrescn  23807  xkoptsub  23822  qtopval  23863  cmphaushmeo  23968  ptcmpg  24225  restutopopn  24406  prdsxmslem2  24697  metuval  24717  nghmfval  24890  isnghm  24891  ismbf1  25794  ismbf  25798  mbfconst  25803  mbfres2  25815  cncombf  25828  isi1f  25844  itg1val  25853  deg1val  26264  fta1glem2  26337  fta1g  26338  fta1b  26340  dgrval  26396  dgrlem  26397  coeidlem  26405  coe11  26421  fta1lem  26479  fta1  26480  vieta1lem2  26483  vieta1  26484  taylthlem2  26548  areaval  27140  sqff1o  27357  seqseq123d  28490  nlfnval  32244  xppreima2  33007  ofpreima  33021  mptiffisupp  33049  fpwrelmapffslem  33088  indf1ofs  33197  evpmval  33474  altgnsg  33478  ply1dg3rt0irred  33883  vieta  33979  xrhval  34417  ismbfm  34650  mbfmcst  34658  issibf  34732  sitgfval  34740  eulerpartlemelr  34756  eulerpartleme  34762  eulerpartlemo  34764  eulerpartlemt0  34768  eulerpartlemt  34770  eulerpartlemr  34773  eulerpartlemgf  34778  eulerpartlemgs2  34779  eulerpartlemn  34780  eulerpart  34781  ballotlemscr  34918  ballotlemrv  34919  ballotlemrinv0  34932  iscvm  35759  cvmliftmolem1  35781  cvmlift2lem9a  35803  cvmlift2lem9  35811  msrfval  36037  ismfs  36049  mthmval  36075  ttcid  37031  bj-imdirval2  37855  bj-iminvval2  37866  poimirlem4  38303  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem13  38312  poimirlem14  38313  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem26  38325  poimirlem27  38326  poimirlem32  38331  cnambfre  38347  itg2addnclem2  38351  ftc1anclem1  38372  ftc1anclem6  38377  lkrval  39890  aks6d1c6lem4  42968  aks6d1c6lem5  42972  aks6d1c7lem3  42977  prjcrvfval  43391  prjcrvval  43392  prjcrv0  43393  pw2f1o2val  43794  aomclem8  43816  pwfi2f1o  43851  trclimalb2  44480  frege131d  44518  colleq12d  44991  dirkercncflem2  46846  issmflem  47469  smfpimioo  47529  smfpimcc  47550  smfsuplem2  47554  3f1oss1  47840  imaidfu2lem  49915  imaidfu  49916  imaidfu2  49917