Theorem fveqeq2d 6899

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551

This theorem is referenced by:  fveqeq2  6900  op1stg  7989  op2ndg  7990  ttrclss  9717  ttrclselem2  9723  fpwwecbv  10641  fpwwelem  10642  fseq1m1p1  13578  ico01fl0  13786  divfl0  13791  hashssdif  14374  cshw1  14774  smumullem  16435  algcvga  16518  vdwlem6  16921  vdwlem8  16923  ramub1lem1  16961  resmhm  18703  isghm  19094  fislw  19495  pgpfaclem2  19954  abvfval  20430  abvpropd  20454  lspsneq0  20628  reslmhm  20668  lspsneq  20741  mdetunilem7  22127  imasdsf1olem  23886  bcth  24853  ovoliunnul  25031  lognegb  26105  vmaval  26624  2lgslem3c  26908  2lgslem3d  26909  rusgrnumwrdl2  28881  wlkiswwlks2  29167  rusgrnumwwlks  29266  clwlkclwwlklem1  29290  clwlkclwwlklem2  29291  numclwwlk1  29652  wlkl0  29658  numclwlk1lem1  29660  isnvlem  29901  lnoval  30043  normsub0  30427  elunop2  31304  ishst  31505  hstri  31556  aciunf1lem  31925  lmatfval  32863  lmatcl  32865  voliune  33296  volfiniune  33297  snmlval  34391  voliunnfl  36618  sdclem1  36697  islshp  37935  lshpnel2N  37941  lshpset2N  38075  dicffval  40131  dicfval  40132  mapdhval  40681  hdmap1fval  40753  hdmap1vallem  40754  hdmap1val  40755  diophin  41592  eldioph4b  41631  eldioph4i  41632  diophren  41633  fperiodmullem  44092  fargshiftfva  46190  paireqne  46258  resmgmhm  46647  0ringdif  46723