Theorem imaeq1d 6057

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

Syntax hints:   → wi 4   = wceq 1539   “ cima 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688

This theorem is referenced by:  imaeq12d  6059  nfimad  6067  csbrn  6201  f1imacnv  6848  foimacnv  6849  fimacnvinrn  7072  seqomeq12  8456  ssenen  9153  fipreima  9360  oieq1  9509  oieq2  9510  dfac12lem1  10140  dfac12r  10143  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwecbv  10641  fpwwelem  10642  seqeq1  13973  seqeq2  13974  seqeq3  13975  1arith  16864  vdwmc  16915  vdwnnlem1  16932  ramub2  16951  rami  16952  imasless  17490  gsumvalx  18601  eqglact  19095  eqg0subgecsn  19112  psgnunilem1  19402  evpmss  21358  psgnevpmb  21359  frlmup3  21574  psrbag  21689  psrbaglefi  21704  psrbaglefiOLD  21705  iscn  22959  ptbasfi  23305  ptval2  23325  ptrescn  23363  xkoptsub  23378  qtopval  23419  cmphaushmeo  23524  ptcmpg  23781  restutopopn  23963  prdsxmslem2  24258  metuval  24278  nghmfval  24459  isnghm  24460  ismbf1  25373  ismbf  25377  mbfconst  25382  mbfres2  25394  cncombf  25407  isi1f  25423  itg1val  25432  deg1val  25849  fta1glem2  25919  fta1g  25920  fta1b  25922  dgrval  25977  dgrlem  25978  coeidlem  25986  coe11  26002  fta1lem  26056  fta1  26057  vieta1lem2  26060  vieta1  26061  taylthlem2  26122  areaval  26705  sqff1o  26922  nlfnval  31401  xppreima2  32143  ofpreima  32157  mptiffisupp  32182  fpwrelmapffslem  32224  evpmval  32574  altgnsg  32578  xrhval  33296  indf1ofs  33322  ismbfm  33547  mbfmcst  33556  issibf  33630  sitgfval  33638  eulerpartlemelr  33654  eulerpartleme  33660  eulerpartlemo  33662  eulerpartlemt0  33666  eulerpartlemt  33668  eulerpartlemr  33671  eulerpartlemgf  33676  eulerpartlemgs2  33677  eulerpartlemn  33678  eulerpart  33679  ballotlemscr  33815  ballotlemrv  33816  ballotlemrinv0  33829  iscvm  34548  cvmliftmolem1  34570  cvmlift2lem9a  34592  cvmlift2lem9  34600  msrfval  34826  ismfs  34838  mthmval  34864  bj-imdirval2  36367  bj-iminvval2  36378  poimirlem4  36795  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem13  36804  poimirlem14  36805  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem18  36809  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem26  36817  poimirlem27  36818  poimirlem32  36823  cnambfre  36839  itg2addnclem2  36843  ftc1anclem1  36864  ftc1anclem6  36869  lkrval  38261  prjcrvfval  41675  prjcrvval  41676  prjcrv0  41677  pw2f1o2val  42080  aomclem8  42105  pwfi2f1o  42140  trclimalb2  42779  frege131d  42817  colleq12d  43314  dirkercncflem2  45118  issmflem  45741  smfpimioo  45801  smfpimcc  45822  smfsuplem2  45826