Theorem imaeq1d 6018

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

Syntax hints:   → wi 4   = wceq 1547   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  imaeq12d  6020  nfimad  6028  csbrn  6161  f1imacnv  6790  foimacnv  6791  fimacnvinrn  7019  seqomeq12  8390  ssenen  9086  fipreima  9265  oieq1  9424  oieq2  9425  dfac12lem1  10064  dfac12r  10067  fpwwe2cbv  10551  fpwwe2lem2  10553  fpwwecbv  10565  fpwwelem  10566  seqeq1  13964  seqeq2  13965  seqeq3  13966  1arith  16896  vdwmc  16947  vdwnnlem1  16964  ramub2  16983  rami  16984  imasless  17502  gsumvalx  18642  eqglact  19152  eqg0subgecsn  19170  psgnunilem1  19466  evpmss  21568  psgnevpmb  21569  frlmup3  21782  psrbag  21899  psrbaglefi  21908  iscn  23225  ptbasfi  23571  ptval2  23591  ptrescn  23629  xkoptsub  23644  qtopval  23685  cmphaushmeo  23790  ptcmpg  24047  restutopopn  24228  prdsxmslem2  24519  metuval  24539  nghmfval  24712  isnghm  24713  ismbf1  25616  ismbf  25620  mbfconst  25625  mbfres2  25637  cncombf  25650  isi1f  25666  itg1val  25675  deg1val  26086  fta1glem2  26159  fta1g  26160  fta1b  26162  dgrval  26218  dgrlem  26219  coeidlem  26227  coe11  26243  fta1lem  26298  fta1  26299  vieta1lem2  26302  vieta1  26303  taylthlem2  26364  areaval  26953  sqff1o  27170  seqseq123d  28303  nlfnval  31977  xppreima2  32750  ofpreima  32764  mptiffisupp  32792  fpwrelmapffslem  32831  indf1ofs  32952  evpmval  33233  altgnsg  33237  ply1dg3rt0irred  33674  vieta  33771  xrhval  34209  ismbfm  34442  mbfmcst  34450  issibf  34524  sitgfval  34532  eulerpartlemelr  34548  eulerpartleme  34554  eulerpartlemo  34556  eulerpartlemt0  34560  eulerpartlemt  34562  eulerpartlemr  34565  eulerpartlemgf  34570  eulerpartlemgs2  34571  eulerpartlemn  34572  eulerpart  34573  ballotlemscr  34710  ballotlemrv  34711  ballotlemrinv0  34724  iscvm  35494  cvmliftmolem1  35516  cvmlift2lem9a  35538  cvmlift2lem9  35546  msrfval  35772  ismfs  35784  mthmval  35810  ttcid  36727  bj-imdirval2  37550  bj-iminvval2  37561  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem14  38008  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem26  38020  poimirlem27  38021  poimirlem32  38026  cnambfre  38042  itg2addnclem2  38046  ftc1anclem1  38067  ftc1anclem6  38072  lkrval  39587  aks6d1c6lem4  42665  aks6d1c6lem5  42669  aks6d1c7lem3  42674  prjcrvfval  43088  prjcrvval  43089  prjcrv0  43090  pw2f1o2val  43491  aomclem8  43513  pwfi2f1o  43548  trclimalb2  44177  frege131d  44215  colleq12d  44704  dirkercncflem2  46554  issmflem  47177  smfpimioo  47237  smfpimcc  47258  smfsuplem2  47262  3f1oss1  47545  imaidfu2lem  49606  imaidfu  49607  imaidfu2  49608