Theorem fveqeq2d 6678

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  fveqeq2  6679  op1stg  7701  op2ndg  7702  fpwwecbv  10066  fpwwelem  10067  fseq1m1p1  12983  ico01fl0  13190  divfl0  13195  hashssdif  13774  cshw1  14184  smumullem  15841  algcvga  15923  vdwlem6  16322  vdwlem8  16324  ramub1lem1  16362  resmhm  17985  isghm  18358  fislw  18750  pgpfaclem2  19204  abvfval  19589  abvpropd  19613  lspsneq0  19784  reslmhm  19824  lspsneq  19894  mdetunilem7  21227  imasdsf1olem  22983  bcth  23932  ovoliunnul  24108  lognegb  25173  vmaval  25690  2lgslem3c  25974  2lgslem3d  25975  rusgrnumwrdl2  27368  wlkiswwlks2  27653  rusgrnumwwlks  27753  clwlkclwwlklem1  27777  clwlkclwwlklem2  27778  numclwwlk1  28140  wlkl0  28146  numclwlk1lem1  28148  isnvlem  28387  lnoval  28529  normsub0  28913  elunop2  29790  ishst  29991  hstri  30042  aciunf1lem  30407  lmatfval  31079  lmatcl  31081  voliune  31488  volfiniune  31489  snmlval  32578  voliunnfl  34951  sdclem1  35033  islshp  36130  lshpnel2N  36136  lshpset2N  36270  dicffval  38325  dicfval  38326  mapdhval  38875  hdmap1fval  38947  hdmap1vallem  38948  hdmap1val  38949  diophin  39418  eldioph4b  39457  eldioph4i  39458  diophren  39459  fperiodmullem  41619  fargshiftfva  43652  paireqne  43722  resmgmhm  44114  0ringdif  44190