Theorem imaeq1d 6067

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-cnv 5664  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669

This theorem is used by:  imaeq12d  6069  nfimad  6081  csbrn  6221  f1imacnv  6869  foimacnv  6870  fimacnvinrn  7101  seqomeq12  8500  ssenen  9206  fipreima  9383  oieq1  9541  oieq2  9542  dfac12lem1  10259  dfac12r  10262  fpwwe2cbv  10752  fpwwe2lem2  10754  fpwwecbv  10766  fpwwelem  10767  seqeq1  14185  seqeq2  14186  seqeq3  14187  1arith  17146  vdwmc  17197  vdwnnlem1  17214  ramub2  17233  rami  17234  imasless  17753  gsumvalx  18906  eqglact  19432  eqg0subgecsn  19453  psgnunilem1  19749  evpmss  21936  psgnevpmb  21937  frlmup3  22150  psrbag  22269  psrbaglefi  22278  iscn  23597  ptbasfi  23944  ptval2  23964  ptrescn  24002  xkoptsub  24017  qtopval  24058  cmphaushmeo  24163  ptcmpg  24420  restutopopn  24601  prdsxmslem2  24892  metuval  24912  nghmfval  25085  isnghm  25086  ismbf1  25989  ismbf  25993  mbfconst  25998  mbfres2  26010  cncombf  26023  isi1f  26039  itg1val  26048  deg1val  26458  fta1glem2  26531  fta1g  26532  fta1b  26534  dgrval  26591  dgrlem  26592  coeidlem  26600  coe11  26616  fta1lem  26672  fta1  26673  vieta1lem2  26678  vieta1  26679  taylthlem2  26747  areaval  27338  sqff1o  27555  seqseq123d  28718  nlfnval  32529  xppreima2  33333  ofpreima  33347  mptiffisupp  33373  fpwrelmapffslem  33410  indf1ofs  33519  evpmval  33795  altgnsg  33799  ply1dg3rt0irred  34212  vieta  34316  xrhval  34754  ismbfm  34988  mbfmcst  34995  issibf  35069  sitgfval  35077  eulerpartlemelr  35093  eulerpartleme  35099  eulerpartlemo  35101  eulerpartlemt0  35105  eulerpartlemt  35107  eulerpartlemr  35110  eulerpartlemgf  35115  eulerpartlemgs2  35116  eulerpartlemn  35117  eulerpart  35118  ballotlemscr  35255  ballotlemrv  35256  ballotlemrinv0  35269  iscvm  36225  cvmliftmolem1  36247  cvmlift2lem9a  36269  cvmlift2lem9  36277  msrfval  36503  ismfs  36515  mthmval  36541  ttcid  37488  bj-imdirval2  38365  bj-iminvval2  38376  poimirlem4  38803  poimirlem5  38804  poimirlem6  38805  poimirlem7  38806  poimirlem8  38807  poimirlem10  38809  poimirlem11  38810  poimirlem12  38811  poimirlem13  38812  poimirlem14  38813  poimirlem15  38814  poimirlem16  38815  poimirlem17  38816  poimirlem18  38817  poimirlem19  38818  poimirlem20  38819  poimirlem21  38820  poimirlem22  38821  poimirlem26  38825  poimirlem27  38826  poimirlem32  38831  cnambfre  38847  itg2addnclem2  38851  ftc1anclem1  38872  ftc1anclem6  38877  lkrval  40404  aks6d1c6lem4  43482  aks6d1c6lem5  43486  aks6d1c7lem3  43491  prjcrvfval  43927  prjcrvval  43928  prjcrv0  43929  pw2f1o2val  44306  aomclem8  44323  pwfi2f1o  44358  trclimalb2  44981  frege131d  45019  colleq12d  45492  dirkercncflem2  47381  issmflem  48004  smfpimioo  48064  smfpimcc  48085  smfsuplem2  48089  3f1oss1  48412  imaidfu2lem  50550  imaidfu  50551  imaidfu2  50552