Theorem fveqeq2d 6914

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 6910	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	2	eqeq1d 2736	1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570

This theorem is referenced by:  fveqeq2  6915  op1stg  8024  op2ndg  8025  ttrclss  9757  ttrclselem2  9763  fpwwecbv  10681  fpwwelem  10682  fseq1m1p1  13635  ico01fl0  13855  divfl0  13860  hashssdif  14447  cshw1  14856  smumullem  16525  algcvga  16612  vdwlem6  17019  vdwlem8  17021  ramub1lem1  17059  resmgmhm  18736  resmhm  18845  isghmOLD  19246  fislw  19657  pgpfaclem2  20116  0ringdif  20543  abvfval  20827  abvpropd  20852  lspsneq0  21027  reslmhm  21068  lspsneq  21141  mdetunilem7  22639  imasdsf1olem  24398  bcth  25376  ovoliunnul  25555  lognegb  26646  vmaval  27170  2lgslem3c  27456  2lgslem3d  27457  rusgrnumwrdl2  29618  wlkiswwlks2  29904  rusgrnumwwlks  30003  clwlkclwwlklem1  30027  clwlkclwwlklem2  30028  numclwwlk1  30389  wlkl0  30395  numclwlk1lem1  30397  isnvlem  30638  lnoval  30780  normsub0  31164  elunop2  32041  ishst  32242  hstri  32293  aciunf1lem  32678  lmatfval  33774  lmatcl  33776  voliune  34209  volfiniune  34210  snmlval  35315  voliunnfl  37650  sdclem1  37729  islshp  38960  lshpnel2N  38966  lshpset2N  39100  dicffval  41156  dicfval  41157  mapdhval  41706  hdmap1fval  41778  hdmap1vallem  41779  hdmap1val  41780  aks6d1c6isolem1  42155  aks6d1c6lem5  42158  diophin  42759  eldioph4b  42798  eldioph4i  42799  diophren  42800  fperiodmullem  45253  fargshiftfva  47367  paireqne  47435  isuspgrim0  47809  grimidvtxedg  47813  grimcnv  47816  grimco  47817  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838