Theorem fveqeq2d 6848

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507

This theorem is referenced by:  fveqeq2  6849  op1stg  7959  op2ndg  7960  ttrclss  9649  ttrclselem2  9655  fpwwecbv  10573  fpwwelem  10574  fseq1m1p1  13536  ico01fl0  13757  divfl0  13762  hashssdif  14353  cshw1  14763  smumullem  16438  algcvga  16525  vdwlem6  16933  vdwlem8  16935  ramub1lem1  16973  resmgmhm  18620  resmhm  18729  isghmOLD  19130  fislw  19539  pgpfaclem2  19998  0ringdif  20447  abvfval  20730  abvpropd  20755  lspsneq0  20950  reslmhm  20991  lspsneq  21064  mdetunilem7  22538  imasdsf1olem  24294  bcth  25262  ovoliunnul  25441  lognegb  26532  vmaval  27056  2lgslem3c  27342  2lgslem3d  27343  rusgrnumwrdl2  29567  wlkiswwlks2  29855  rusgrnumwwlks  29954  clwlkclwwlklem1  29978  clwlkclwwlklem2  29979  numclwwlk1  30340  wlkl0  30346  numclwlk1lem1  30348  isnvlem  30589  lnoval  30731  normsub0  31115  elunop2  31992  ishst  32193  hstri  32244  aciunf1lem  32636  lmatfval  33797  lmatcl  33799  voliune  34212  volfiniune  34213  snmlval  35311  voliunnfl  37651  sdclem1  37730  islshp  38965  lshpnel2N  38971  lshpset2N  39105  dicffval  41161  dicfval  41162  mapdhval  41711  hdmap1fval  41783  hdmap1vallem  41784  hdmap1val  41785  aks6d1c6isolem1  42155  aks6d1c6lem5  42158  diophin  42753  eldioph4b  42792  eldioph4i  42793  diophren  42794  fperiodmullem  45294  fargshiftfva  47437  paireqne  47505  grimidvtxedg  47878  grimcnv  47881  grimco  47882  isuspgrim0  47887  uhgrimisgrgriclem  47923  clnbgrgrimlem  47926