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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544

This theorem is referenced by:  fveqeq2  6890  op1stg  7994  op2ndg  7995  ttrclss  9685  ttrclselem2  9691  fpwwecbv  10624  fpwwelem  10625  fseq1m1p1  13623  ico01fl0  13848  divfl0  13853  hashssdif  14445  cshw1  14855  smumullem  16545  algcvga  16632  vdwlem6  17041  vdwlem8  17043  ramub1lem1  17081  resmgmhm  18764  resmhm  18874  fislw  19690  pgpfaclem2  20149  0ringdif  20625  abvfval  20913  abvpropd  20938  lspsneq0  21133  reslmhm  21173  lspsneq  21246  mdetunilem7  22775  imasdsf1olem  24530  bcth  25488  ovoliunnul  25666  lognegb  26755  vmaval  27277  2lgslem3c  27562  2lgslem3d  27563  rusgrnumwrdl2  29936  wlkiswwlks2  30224  rusgrnumwwlks  30326  clwlkclwwlklem1  30350  clwlkclwwlklem2  30351  numclwwlk1  30712  wlkl0  30718  numclwlk1lem1  30720  isnvlem  30962  lnoval  31104  normsub0  31488  elunop2  32365  ishst  32566  hstri  32617  aciunf1lem  33007  esplyfvaln  33964  esplyind  33965  vietadeg1  33968  lmatfval  34204  lmatcl  34206  voliune  34619  volfiniune  34620  snmlval  35823  qdiff  37991  voliunnfl  38335  sdclem1  38414  islshp  39773  lshpnel2N  39779  lshpset2N  39913  dicffval  41968  dicfval  41969  mapdhval  42518  hdmap1fval  42590  hdmap1vallem  42591  hdmap1val  42592  aks6d1c6isolem1  42961  aks6d1c6lem5  42964  diophin  43523  eldioph4b  43558  eldioph4i  43559  diophren  43560  fperiodmullem  46042  fourierdlem48  46888  fourierdlem49  46889  fargshiftfva  48212  paireqne  48280  grimidvtxedg  48670  grimcnv  48673  grimco  48674  isuspgrim0  48679  uhgrimisgrgriclem  48715  clnbgrgrimlem  48718