Theorem fveqeq2d 6893

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 6494  df-fv 6546

This theorem is used by:  fveqeq2  6894  op1stg  8013  op2ndg  8014  ttrclss  9721  ttrclselem2  9727  fpwwecbv  10729  fpwwelem  10730  fseq1m1p1  13733  ico01fl0  13959  divfl0  13964  hashssdif  14557  cshw1  14973  smumullem  16662  algcvga  16754  vdwlem6  17164  vdwlem8  17166  ramub1lem1  17204  resmgmhm  18900  resmhm  19016  fislw  19839  pgpfaclem2  20298  0ringdif  20778  abvfval  21067  abvpropd  21092  lspsneq0  21287  reslmhm  21327  lspsneq  21400  mdetunilem7  22933  imasdsf1olem  24692  bcth  25650  ovoliunnul  25828  lognegb  26918  vmaval  27440  2lgslem3c  27725  2lgslem3d  27726  rusgrnumwrdl2  30167  wlkiswwlks2  30464  rusgrnumwwlks  30566  clwlkclwwlklem1  30590  clwlkclwwlklem2  30591  numclwwlk1  30962  wlkl0  30968  numclwlk1lem1  30970  isnvlem  31212  lnoval  31354  normsub0  31738  elunop2  32615  ishst  32816  hstri  32867  aciunf1lem  33256  esplyfvaln  34206  esplyind  34207  vietadeg1  34210  lmatfval  34446  lmatcl  34448  voliune  34862  volfiniune  34863  snmlval  36096  qdiff  38248  voliunnfl  38582  sdclem1  38677  islshp  40036  lshpnel2N  40042  lshpset2N  40176  dicffval  42231  dicfval  42232  mapdhval  42781  hdmap1fval  42853  hdmap1vallem  42854  hdmap1val  42855  aks6d1c6isolem1  43224  aks6d1c6lem5  43227  diophin  43782  eldioph4b  43817  eldioph4i  43818  diophren  43819  fperiodmullem  46318  fourierdlem48  47163  fourierdlem49  47164  fargshiftfva  48524  paireqne  48592  grimidvtxedg  48982  grimcnv  48985  grimco  48986  isuspgrim0  48991  uhgrimisgrgriclem  49027  clnbgrgrimlem  49030