Theorem fveq2d 2836

Description: Equality deduction for function value.

Hypothesis

Ref	Expression
fveq2d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
fveq2d	⊢ (φ → (F ‘A) = (F ‘B))

Proof of Theorem fveq2d

Step	Hyp	Ref	Expression
1		fveq2d.1	. 2 ⊢ (φ → A = B)
2		fveq2 2832	. 2 ⊢ (A = B → (F ‘A) = (F ‘B))
3	1, 2	syl 12	1 ⊢ (φ → (F ‘A) = (F ‘B))

Syntax hints:   → wi 2   = wceq 1091   ‘cfv 2422

This theorem is referenced by:  tfrlem1 2949  tfrlem3 2951  tfrlem5 2953  tfrlem9 2957  tfrlem11 2959  tfrlem12 2960  tfr2 2963  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  rdglem1 2975  rdglem2 2976  rdgsuct 2983  frsuc 2991  opreq1 3006  opreq2 3007  oprprc2 3020  elrnoprab 3054  oasuc 3131  omsuc 3133  oesuc 3134  omsmolem 3195  xpdom2 3345  inf3lem1 3464  rankid 3516  rankr1 3518  rankr1id 3539  aceq3lem 3555  ac6lem 3575  cardcard 3655  cardiun 3665  alephcard 3673  om2uzsuc 4652  uzrdgsuc 4659  seqlem1 4662  seqrval 4664  seqval 4665  seqval2 4667  seqsuclem 4669  sqrmul 4763  absvalt 4801  cjcjt 4830  cjaddt 4831  cjmult 4832  absmult 4849  abssubt 4864  abs3lemt 4865  abslem2 4867  facp1t 4873  clim 4877  clim2 4881  clim0 4882  ruclem18 4902  ruclem19 4903  ruclem20 4904  ruclem21 4905  ruclem25 4909  ruclem29 4913  ruclem32 4916  his5 5050  his7 5051  hizer2t 5055  normvalt 5075  normgt0t 5078  norm0 5079  normsub0t 5085  norm-iiit 5088  normsubt 5091  normpytht 5092  norm3lemt 5097  norm3adift 5098  bcs 5101  hcauchy 5103  hlim 5108  hlim2 5112  hlim0 5140  hlimcaui 5141  occllem2 5181  occllem6 5185  projlem7 5199  projlem8 5200  projlem10 5202  projlem15 5207  projlem16 5208  projlem17 5209  projlem20 5212  projlem22 5214  projlem23 5215  projlem25 5217  projlem26 5218  projlem28 5220  pjthlem8 5232  pjthlem9 5233  pjthlem12 5236  pjth 5239  ococt 5253  axpjpjt 5260  pjoc1t 5270  sshjvalt 5321  sshjval3t 5327  chdmm1t 5438  chdmj1t 5442  h1de2ctlem 5460  spansnt 5464  elspansnt 5471  elspansn2t 5472  spansneleq 5475  h1datomt 5484  cmcmlem 5500  osumlem2 5531  spansnjt 5540  spansncvt 5543  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  pjsumt 5590  hoid1 5617  pjsdi 5625  pjddi 5626  pjss2co 5634  pjdifnormt 5637  pjssum 5641  pjclem4 5653  pj3s 5659  pjopytht 5662  pjnormt 5666  pjnelt 5667  pjs14 5669  stjt 5676  strlem2 5692  strlem3a 5693  strlem4 5695  stcltrlem1 5709

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438

metamath.org