Theorem imaeq1d 6055

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  imaeq12d  6057  nfimad  6065  csbrn  6199  f1imacnv  6834  foimacnv  6835  fimacnvinrn  7064  seqomeq12  8443  ssenen  9149  fipreima  9325  oieq1  9484  oieq2  9485  dfac12lem1  10146  dfac12r  10149  fpwwe2cbv  10639  fpwwe2lem2  10641  fpwwecbv  10653  fpwwelem  10654  seqeq1  14068  seqeq2  14069  seqeq3  14070  1arith  17019  vdwmc  17070  vdwnnlem1  17087  ramub2  17106  rami  17107  imasless  17626  gsumvalx  18778  eqglact  19304  eqg0subgecsn  19325  psgnunilem1  19620  evpmss  21799  psgnevpmb  21800  frlmup3  22013  psrbag  22132  psrbaglefi  22141  iscn  23460  ptbasfi  23807  ptval2  23827  ptrescn  23865  xkoptsub  23880  qtopval  23921  cmphaushmeo  24026  ptcmpg  24283  restutopopn  24464  prdsxmslem2  24755  metuval  24775  nghmfval  24948  isnghm  24949  ismbf1  25852  ismbf  25856  mbfconst  25861  mbfres2  25873  cncombf  25886  isi1f  25902  itg1val  25911  deg1val  26321  fta1glem2  26394  fta1g  26395  fta1b  26397  dgrval  26454  dgrlem  26455  coeidlem  26463  coe11  26479  fta1lem  26537  fta1  26538  vieta1lem2  26543  vieta1  26544  taylthlem2  26610  areaval  27201  sqff1o  27418  seqseq123d  28551  nlfnval  32362  xppreima2  33124  ofpreima  33138  mptiffisupp  33165  fpwrelmapffslem  33203  indf1ofs  33312  evpmval  33585  altgnsg  33589  ply1dg3rt0irred  33994  vieta  34090  xrhval  34528  ismbfm  34762  mbfmcst  34770  issibf  34844  sitgfval  34852  eulerpartlemelr  34868  eulerpartleme  34874  eulerpartlemo  34876  eulerpartlemt0  34880  eulerpartlemt  34882  eulerpartlemr  34885  eulerpartlemgf  34890  eulerpartlemgs2  34891  eulerpartlemn  34892  eulerpart  34893  ballotlemscr  35030  ballotlemrv  35031  ballotlemrinv0  35044  iscvm  35838  cvmliftmolem1  35860  cvmlift2lem9a  35882  cvmlift2lem9  35890  msrfval  36116  ismfs  36128  mthmval  36154  ttcid  37111  bj-imdirval2  37935  bj-iminvval2  37946  poimirlem4  38373  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem26  38395  poimirlem27  38396  poimirlem32  38401  cnambfre  38417  itg2addnclem2  38421  ftc1anclem1  38442  ftc1anclem6  38447  lkrval  39961  aks6d1c6lem4  43039  aks6d1c6lem5  43043  aks6d1c7lem3  43048  prjcrvfval  43477  prjcrvval  43478  prjcrv0  43479  pw2f1o2val  43880  aomclem8  43902  pwfi2f1o  43937  trclimalb2  44566  frege131d  44604  colleq12d  45077  dirkercncflem2  46932  issmflem  47555  smfpimioo  47615  smfpimcc  47636  smfsuplem2  47640  3f1oss1  47963  imaidfu2lem  50035  imaidfu  50036  imaidfu2  50037