Theorem imaeq1d 6076

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-cnv 5692  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697

This theorem is referenced by:  imaeq12d  6078  nfimad  6086  csbrn  6222  f1imacnv  6863  foimacnv  6864  fimacnvinrn  7090  seqomeq12  8495  ssenen  9192  fipreima  9399  oieq1  9553  oieq2  9554  dfac12lem1  10185  dfac12r  10188  fpwwe2cbv  10671  fpwwe2lem2  10673  fpwwecbv  10685  fpwwelem  10686  seqeq1  14046  seqeq2  14047  seqeq3  14048  1arith  16966  vdwmc  17017  vdwnnlem1  17034  ramub2  17053  rami  17054  imasless  17586  gsumvalx  18690  eqglact  19198  eqg0subgecsn  19216  psgnunilem1  19512  evpmss  21605  psgnevpmb  21606  frlmup3  21821  psrbag  21938  psrbaglefi  21947  iscn  23244  ptbasfi  23590  ptval2  23610  ptrescn  23648  xkoptsub  23663  qtopval  23704  cmphaushmeo  23809  ptcmpg  24066  restutopopn  24248  prdsxmslem2  24543  metuval  24563  nghmfval  24744  isnghm  24745  ismbf1  25660  ismbf  25664  mbfconst  25669  mbfres2  25681  cncombf  25694  isi1f  25710  itg1val  25719  deg1val  26136  fta1glem2  26209  fta1g  26210  fta1b  26212  dgrval  26268  dgrlem  26269  coeidlem  26277  coe11  26293  fta1lem  26350  fta1  26351  vieta1lem2  26354  vieta1  26355  taylthlem2  26417  taylthlem2OLD  26418  areaval  27008  sqff1o  27226  seqseq123d  28293  nlfnval  31901  xppreima2  32662  ofpreima  32676  mptiffisupp  32703  fpwrelmapffslem  32744  indf1ofs  32852  evpmval  33166  altgnsg  33170  ply1dg3rt0irred  33608  xrhval  34020  ismbfm  34253  mbfmcst  34262  issibf  34336  sitgfval  34344  eulerpartlemelr  34360  eulerpartleme  34366  eulerpartlemo  34368  eulerpartlemt0  34372  eulerpartlemt  34374  eulerpartlemr  34377  eulerpartlemgf  34382  eulerpartlemgs2  34383  eulerpartlemn  34384  eulerpart  34385  ballotlemscr  34522  ballotlemrv  34523  ballotlemrinv0  34536  iscvm  35265  cvmliftmolem1  35287  cvmlift2lem9a  35309  cvmlift2lem9  35317  msrfval  35543  ismfs  35555  mthmval  35581  bj-imdirval2  37185  bj-iminvval2  37196  poimirlem4  37632  poimirlem5  37633  poimirlem6  37634  poimirlem7  37635  poimirlem8  37636  poimirlem10  37638  poimirlem11  37639  poimirlem12  37640  poimirlem13  37641  poimirlem14  37642  poimirlem15  37643  poimirlem16  37644  poimirlem17  37645  poimirlem18  37646  poimirlem19  37647  poimirlem20  37648  poimirlem21  37649  poimirlem22  37650  poimirlem26  37654  poimirlem27  37655  poimirlem32  37660  cnambfre  37676  itg2addnclem2  37680  ftc1anclem1  37701  ftc1anclem6  37706  lkrval  39090  aks6d1c6lem4  42175  aks6d1c6lem5  42179  aks6d1c7lem3  42184  prjcrvfval  42646  prjcrvval  42647  prjcrv0  42648  pw2f1o2val  43056  aomclem8  43078  pwfi2f1o  43113  trclimalb2  43744  frege131d  43782  colleq12d  44277  dirkercncflem2  46124  issmflem  46747  smfpimioo  46807  smfpimcc  46828  smfsuplem2  46832  3f1oss1  47092