Theorem fveqeq2d 6653

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ‘cfv 6324

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332

This theorem is referenced by:  fveqeq2  6654  op1stg  7683  op2ndg  7684  fpwwecbv  10055  fpwwelem  10056  fseq1m1p1  12977  ico01fl0  13184  divfl0  13189  hashssdif  13769  cshw1  14175  smumullem  15831  algcvga  15913  vdwlem6  16312  vdwlem8  16314  ramub1lem1  16352  resmhm  17977  isghm  18350  fislw  18742  pgpfaclem2  19197  abvfval  19582  abvpropd  19606  lspsneq0  19777  reslmhm  19817  lspsneq  19887  mdetunilem7  21223  imasdsf1olem  22980  bcth  23933  ovoliunnul  24111  lognegb  25181  vmaval  25698  2lgslem3c  25982  2lgslem3d  25983  rusgrnumwrdl2  27376  wlkiswwlks2  27661  rusgrnumwwlks  27760  clwlkclwwlklem1  27784  clwlkclwwlklem2  27785  numclwwlk1  28146  wlkl0  28152  numclwlk1lem1  28154  isnvlem  28393  lnoval  28535  normsub0  28919  elunop2  29796  ishst  29997  hstri  30048  aciunf1lem  30425  lmatfval  31167  lmatcl  31169  voliune  31598  volfiniune  31599  snmlval  32691  voliunnfl  35101  sdclem1  35181  islshp  36275  lshpnel2N  36281  lshpset2N  36415  dicffval  38470  dicfval  38471  mapdhval  39020  hdmap1fval  39092  hdmap1vallem  39093  hdmap1val  39094  diophin  39713  eldioph4b  39752  eldioph4i  39753  diophren  39754  fperiodmullem  41935  fargshiftfva  43960  paireqne  44028  resmgmhm  44418  0ringdif  44494