Theorem fveqeq2d 6889

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544

This theorem is used by:  fveqeq2  6890  op1stg  7996  op2ndg  7997  ttrclss  9687  ttrclselem2  9693  fpwwecbv  10635  fpwwelem  10636  fseq1m1p1  13634  ico01fl0  13859  divfl0  13864  hashssdif  14456  cshw1  14866  smumullem  16556  algcvga  16643  vdwlem6  17052  vdwlem8  17054  ramub1lem1  17092  resmgmhm  18775  resmhm  18885  fislw  19701  pgpfaclem2  20160  0ringdif  20636  abvfval  20924  abvpropd  20949  lspsneq0  21144  reslmhm  21184  lspsneq  21257  mdetunilem7  22786  imasdsf1olem  24541  bcth  25499  ovoliunnul  25677  lognegb  26766  vmaval  27288  2lgslem3c  27573  2lgslem3d  27574  rusgrnumwrdl2  29947  wlkiswwlks2  30235  rusgrnumwwlks  30337  clwlkclwwlklem1  30361  clwlkclwwlklem2  30362  numclwwlk1  30723  wlkl0  30729  numclwlk1lem1  30731  isnvlem  30973  lnoval  31115  normsub0  31499  elunop2  32376  ishst  32577  hstri  32628  aciunf1lem  33018  esplyfvaln  33973  esplyind  33974  vietadeg1  33977  lmatfval  34213  lmatcl  34215  voliune  34628  volfiniune  34629  snmlval  35831  qdiff  37999  voliunnfl  38343  sdclem1  38422  islshp  39781  lshpnel2N  39787  lshpset2N  39921  dicffval  41976  dicfval  41977  mapdhval  42526  hdmap1fval  42598  hdmap1vallem  42599  hdmap1val  42600  aks6d1c6isolem1  42969  aks6d1c6lem5  42972  diophin  43531  eldioph4b  43566  eldioph4i  43567  diophren  43568  fperiodmullem  46050  fourierdlem48  46896  fourierdlem49  46897  fargshiftfva  48220  paireqne  48288  grimidvtxedg  48678  grimcnv  48681  grimco  48682  isuspgrim0  48687  uhgrimisgrgriclem  48723  clnbgrgrimlem  48726