Theorem fveqeq2d 6876

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561  ‘cfv 6522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6478  df-fv 6530

This theorem is referenced by:  fveqeq2  6877  op1stg  7983  op2ndg  7984  ttrclss  9676  ttrclselem2  9682  fpwwecbv  10603  fpwwelem  10604  fseq1m1p1  13605  ico01fl0  13830  divfl0  13835  hashssdif  14426  cshw1  14836  smumullem  16527  algcvga  16614  vdwlem6  17023  vdwlem8  17025  ramub1lem1  17063  resmgmhm  18746  resmhm  18855  fislw  19666  pgpfaclem2  20125  0ringdif  20578  abvfval  20860  abvpropd  20885  lspsneq0  21080  reslmhm  21120  lspsneq  21193  mdetunilem7  22679  imasdsf1olem  24434  bcth  25392  ovoliunnul  25570  lognegb  26656  vmaval  27178  2lgslem3c  27463  2lgslem3d  27464  rusgrnumwrdl2  29788  wlkiswwlks2  30076  rusgrnumwwlks  30178  clwlkclwwlklem1  30202  clwlkclwwlklem2  30203  numclwwlk1  30564  wlkl0  30570  numclwlk1lem1  30572  isnvlem  30814  lnoval  30956  normsub0  31340  elunop2  32217  ishst  32418  hstri  32469  aciunf1lem  32865  esplyfvaln  33872  esplyind  33873  vietadeg1  33876  lmatfval  34112  lmatcl  34114  voliune  34527  volfiniune  34528  snmlval  35682  qdiff  37820  voliunnfl  38164  sdclem1  38243  islshp  39604  lshpnel2N  39610  lshpset2N  39744  dicffval  41799  dicfval  41800  mapdhval  42349  hdmap1fval  42421  hdmap1vallem  42422  hdmap1val  42423  aks6d1c6isolem1  42792  aks6d1c6lem5  42795  diophin  43354  eldioph4b  43389  eldioph4i  43390  diophren  43391  fperiodmullem  45883  fourierdlem48  46729  fourierdlem49  46730  fargshiftfva  48050  paireqne  48118  grimidvtxedg  48508  grimcnv  48511  grimco  48512  isuspgrim0  48517  uhgrimisgrgriclem  48553  clnbgrgrimlem  48556