Theorem imaeq1d 5384

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

Syntax hints:   → wi 4   = wceq 1475   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  imaeq12d  5386  nfimad  5394  csbrn  5514  f1imacnv  6066  foimacnv  6067  fimacnvinrn  6256  seqomeq12  7436  ssenen  8019  fipreima  8155  oieq1  8300  oieq2  8301  dfac12lem1  8848  dfac12r  8851  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwecbv  9345  fpwwelem  9346  seqeq1  12666  seqeq2  12667  seqeq3  12668  1arith  15469  vdwmc  15520  vdwnnlem1  15537  ramub2  15556  rami  15557  imasless  16023  gsumvalx  17093  eqglact  17468  psgnunilem1  17736  psrbag  19185  psrbaglefi  19193  evpmss  19751  psgnevpmb  19752  frlmup3  19958  iscn  20849  ptbasfi  21194  ptval2  21214  ptrescn  21252  xkoptsub  21267  qtopval  21308  cmphaushmeo  21413  ptcmpg  21671  restutopopn  21852  prdsxmslem2  22144  metuval  22164  nghmfval  22336  isnghm  22337  ismbf1  23199  ismbf  23203  mbfconst  23208  mbfres2  23218  cncombf  23231  isi1f  23247  itg1val  23256  deg1val  23660  fta1glem2  23730  fta1g  23731  fta1b  23733  dgrval  23788  dgrlem  23789  coeidlem  23797  coe11  23813  fta1lem  23866  fta1  23867  vieta1lem2  23870  vieta1  23871  taylthlem2  23932  areaval  24491  sqff1o  24708  nlfnval  28124  xppreima2  28830  ofpreima  28848  fpwrelmapffslem  28895  xrhval  29390  indf1ofs  29415  ismbfm  29641  mbfmcst  29648  issibf  29722  sitgfval  29730  eulerpartlemelr  29746  eulerpartleme  29752  eulerpartlemo  29754  eulerpartlemt0  29758  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemgf  29768  eulerpartlemgs2  29769  eulerpartlemn  29770  eulerpart  29771  ballotlemscr  29907  ballotlemrv  29908  ballotlemrinv0  29921  iscvm  30495  cvmliftmolem1  30517  cvmlift2lem9a  30539  cvmlift2lem9  30547  msrfval  30688  ismfs  30700  mthmval  30726  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem26  32605  poimirlem27  32606  poimirlem32  32611  cnambfre  32628  itg2addnclem2  32632  ftc1anclem1  32655  ftc1anclem6  32660  lkrval  33393  pw2f1o2val  36624  aomclem8  36649  pwfi2f1o  36684  trclimalb2  37037  frege131d  37075  dirkercncflem2  38997  issmflem  39613  smfpimioo  39672