Theorem fveqeq2d 6901

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554

This theorem is used by:  fveqeq2  6902  op1stg  8020  op2ndg  8021  ttrclss  9731  ttrclselem2  9737  fpwwecbv  10739  fpwwelem  10740  fseq1m1p1  13743  ico01fl0  13969  divfl0  13974  hashssdif  14567  cshw1  14984  smumullem  16674  algcvga  16766  vdwlem6  17176  vdwlem8  17178  ramub1lem1  17216  resmgmhm  18912  resmhm  19028  fislw  19851  pgpfaclem2  20310  0ringdif  20790  abvfval  21079  abvpropd  21104  lspsneq0  21299  reslmhm  21339  lspsneq  21412  mdetunilem7  22945  imasdsf1olem  24704  bcth  25662  ovoliunnul  25840  lognegb  26930  vmaval  27452  2lgslem3c  27737  2lgslem3d  27738  rusgrnumwrdl2  30179  wlkiswwlks2  30476  rusgrnumwwlks  30578  clwlkclwwlklem1  30602  clwlkclwwlklem2  30603  numclwwlk1  30974  wlkl0  30980  numclwlk1lem1  30982  isnvlem  31224  lnoval  31366  normsub0  31750  elunop2  32627  ishst  32828  hstri  32879  aciunf1lem  33310  esplyfvaln  34259  esplyind  34260  vietadeg1  34263  lmatfval  34499  lmatcl  34501  voliune  34915  volfiniune  34916  snmlval  36217  qdiff  38388  voliunnfl  38722  sdclem1  38817  islshp  40176  lshpnel2N  40182  lshpset2N  40316  dicffval  42371  dicfval  42372  mapdhval  42921  hdmap1fval  42993  hdmap1vallem  42994  hdmap1val  42995  aks6d1c6isolem1  43364  aks6d1c6lem5  43367  diophin  43923  eldioph4b  43958  eldioph4i  43959  diophren  43960  fperiodmullem  46458  fourierdlem48  47303  fourierdlem49  47304  fargshiftfva  48664  paireqne  48732  grimidvtxedg  49122  grimcnv  49125  grimco  49126  isuspgrim0  49131  uhgrimisgrgriclem  49167  clnbgrgrimlem  49170