Theorem fveqeq2d 6869

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522

This theorem is referenced by:  fveqeq2  6870  op1stg  7983  op2ndg  7984  ttrclss  9680  ttrclselem2  9686  fpwwecbv  10604  fpwwelem  10605  fseq1m1p1  13567  ico01fl0  13788  divfl0  13793  hashssdif  14384  cshw1  14794  smumullem  16469  algcvga  16556  vdwlem6  16964  vdwlem8  16966  ramub1lem1  17004  resmgmhm  18645  resmhm  18754  isghmOLD  19155  fislw  19562  pgpfaclem2  20021  0ringdif  20443  abvfval  20726  abvpropd  20751  lspsneq0  20925  reslmhm  20966  lspsneq  21039  mdetunilem7  22512  imasdsf1olem  24268  bcth  25236  ovoliunnul  25415  lognegb  26506  vmaval  27030  2lgslem3c  27316  2lgslem3d  27317  rusgrnumwrdl2  29521  wlkiswwlks2  29812  rusgrnumwwlks  29911  clwlkclwwlklem1  29935  clwlkclwwlklem2  29936  numclwwlk1  30297  wlkl0  30303  numclwlk1lem1  30305  isnvlem  30546  lnoval  30688  normsub0  31072  elunop2  31949  ishst  32150  hstri  32201  aciunf1lem  32593  lmatfval  33811  lmatcl  33813  voliune  34226  volfiniune  34227  snmlval  35325  voliunnfl  37665  sdclem1  37744  islshp  38979  lshpnel2N  38985  lshpset2N  39119  dicffval  41175  dicfval  41176  mapdhval  41725  hdmap1fval  41797  hdmap1vallem  41798  hdmap1val  41799  aks6d1c6isolem1  42169  aks6d1c6lem5  42172  diophin  42767  eldioph4b  42806  eldioph4i  42807  diophren  42808  fperiodmullem  45308  fargshiftfva  47448  paireqne  47516  grimidvtxedg  47889  grimcnv  47892  grimco  47893  isuspgrim0  47898  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937