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 2728	1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6489  df-fv 6545

This theorem is referenced by:  fveqeq2  6894  op1stg  7986  op2ndg  7987  ttrclss  9717  ttrclselem2  9723  fpwwecbv  10641  fpwwelem  10642  fseq1m1p1  13582  ico01fl0  13790  divfl0  13795  hashssdif  14377  cshw1  14778  smumullem  16440  algcvga  16523  vdwlem6  16928  vdwlem8  16930  ramub1lem1  16968  resmgmhm  18644  resmhm  18745  isghm  19141  fislw  19545  pgpfaclem2  20004  0ringdif  20427  abvfval  20661  abvpropd  20685  lspsneq0  20859  reslmhm  20900  lspsneq  20973  mdetunilem7  22475  imasdsf1olem  24234  bcth  25212  ovoliunnul  25391  lognegb  26479  vmaval  27000  2lgslem3c  27286  2lgslem3d  27287  rusgrnumwrdl2  29352  wlkiswwlks2  29638  rusgrnumwwlks  29737  clwlkclwwlklem1  29761  clwlkclwwlklem2  29762  numclwwlk1  30123  wlkl0  30129  numclwlk1lem1  30131  isnvlem  30372  lnoval  30514  normsub0  30898  elunop2  31775  ishst  31976  hstri  32027  aciunf1lem  32396  lmatfval  33324  lmatcl  33326  voliune  33757  volfiniune  33758  snmlval  34850  voliunnfl  37045  sdclem1  37124  islshp  38362  lshpnel2N  38368  lshpset2N  38502  dicffval  40558  dicfval  40559  mapdhval  41108  hdmap1fval  41180  hdmap1vallem  41181  hdmap1val  41182  diophin  42088  eldioph4b  42127  eldioph4i  42128  diophren  42129  fperiodmullem  44585  fargshiftfva  46683  paireqne  46751