Theorem fveqeq2d 6842

Description: Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.)

Hypothesis

Ref	Expression
fveqeq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fveqeq2d	⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Proof of Theorem fveqeq2d

Step	Hyp	Ref	Expression
1		fveqeq2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	fveq2d 6838	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	2	eqeq1d 2738	1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500

This theorem is referenced by:  fveqeq2  6843  op1stg  7945  op2ndg  7946  ttrclss  9629  ttrclselem2  9635  fpwwecbv  10555  fpwwelem  10556  fseq1m1p1  13515  ico01fl0  13739  divfl0  13744  hashssdif  14335  cshw1  14745  smumullem  16419  algcvga  16506  vdwlem6  16914  vdwlem8  16916  ramub1lem1  16954  resmgmhm  18636  resmhm  18745  isghmOLD  19145  fislw  19554  pgpfaclem2  20013  0ringdif  20460  abvfval  20743  abvpropd  20768  lspsneq0  20963  reslmhm  21004  lspsneq  21077  mdetunilem7  22562  imasdsf1olem  24317  bcth  25285  ovoliunnul  25464  lognegb  26555  vmaval  27079  2lgslem3c  27365  2lgslem3d  27366  rusgrnumwrdl2  29660  wlkiswwlks2  29948  rusgrnumwwlks  30050  clwlkclwwlklem1  30074  clwlkclwwlklem2  30075  numclwwlk1  30436  wlkl0  30442  numclwlk1lem1  30444  isnvlem  30685  lnoval  30827  normsub0  31211  elunop2  32088  ishst  32289  hstri  32340  aciunf1lem  32740  esplyind  33731  vietadeg1  33734  lmatfval  33971  lmatcl  33973  voliune  34386  volfiniune  34387  snmlval  35525  voliunnfl  37861  sdclem1  37940  islshp  39235  lshpnel2N  39241  lshpset2N  39375  dicffval  41430  dicfval  41431  mapdhval  41980  hdmap1fval  42052  hdmap1vallem  42053  hdmap1val  42054  aks6d1c6isolem1  42424  aks6d1c6lem5  42427  diophin  43010  eldioph4b  43049  eldioph4i  43050  diophren  43051  fperiodmullem  45547  fargshiftfva  47685  paireqne  47753  grimidvtxedg  48127  grimcnv  48130  grimco  48131  isuspgrim0  48136  uhgrimisgrgriclem  48172  clnbgrgrimlem  48175