Theorem fveqeq2d 6887

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541

This theorem is used by:  fveqeq2  6888  op1stg  7999  op2ndg  8000  ttrclss  9702  ttrclselem2  9708  fpwwecbv  10656  fpwwelem  10657  fseq1m1p1  13657  ico01fl0  13883  divfl0  13888  hashssdif  14480  cshw1  14896  smumullem  16585  algcvga  16672  vdwlem6  17081  vdwlem8  17083  ramub1lem1  17121  resmgmhm  18816  resmhm  18932  fislw  19755  pgpfaclem2  20214  0ringdif  20691  abvfval  20979  abvpropd  21004  lspsneq0  21199  reslmhm  21239  lspsneq  21312  mdetunilem7  22843  imasdsf1olem  24602  bcth  25560  ovoliunnul  25738  lognegb  26830  vmaval  27352  2lgslem3c  27637  2lgslem3d  27638  rusgrnumwrdl2  30049  wlkiswwlks2  30346  rusgrnumwwlks  30448  clwlkclwwlklem1  30472  clwlkclwwlklem2  30473  numclwwlk1  30844  wlkl0  30850  numclwlk1lem1  30852  isnvlem  31094  lnoval  31236  normsub0  31620  elunop2  32497  ishst  32698  hstri  32749  aciunf1lem  33138  esplyfvaln  34087  esplyind  34088  vietadeg1  34091  lmatfval  34327  lmatcl  34329  voliune  34743  volfiniune  34744  snmlval  35913  qdiff  38082  voliunnfl  38416  sdclem1  38496  islshp  39855  lshpnel2N  39861  lshpset2N  39995  dicffval  42050  dicfval  42051  mapdhval  42600  hdmap1fval  42672  hdmap1vallem  42673  hdmap1val  42674  aks6d1c6isolem1  43043  aks6d1c6lem5  43046  diophin  43620  eldioph4b  43655  eldioph4i  43656  diophren  43657  fperiodmullem  46139  fourierdlem48  46985  fourierdlem49  46986  fargshiftfva  48346  paireqne  48414  grimidvtxedg  48804  grimcnv  48807  grimco  48808  isuspgrim0  48813  uhgrimisgrgriclem  48849  clnbgrgrimlem  48852