Theorem fveqeq2d 6914

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569

This theorem is referenced by:  fveqeq2  6915  op1stg  8026  op2ndg  8027  ttrclss  9760  ttrclselem2  9766  fpwwecbv  10684  fpwwelem  10685  fseq1m1p1  13639  ico01fl0  13859  divfl0  13864  hashssdif  14451  cshw1  14860  smumullem  16529  algcvga  16616  vdwlem6  17024  vdwlem8  17026  ramub1lem1  17064  resmgmhm  18724  resmhm  18833  isghmOLD  19234  fislw  19643  pgpfaclem2  20102  0ringdif  20527  abvfval  20811  abvpropd  20836  lspsneq0  21010  reslmhm  21051  lspsneq  21124  mdetunilem7  22624  imasdsf1olem  24383  bcth  25363  ovoliunnul  25542  lognegb  26632  vmaval  27156  2lgslem3c  27442  2lgslem3d  27443  rusgrnumwrdl2  29604  wlkiswwlks2  29895  rusgrnumwwlks  29994  clwlkclwwlklem1  30018  clwlkclwwlklem2  30019  numclwwlk1  30380  wlkl0  30386  numclwlk1lem1  30388  isnvlem  30629  lnoval  30771  normsub0  31155  elunop2  32032  ishst  32233  hstri  32284  aciunf1lem  32672  lmatfval  33813  lmatcl  33815  voliune  34230  volfiniune  34231  snmlval  35336  voliunnfl  37671  sdclem1  37750  islshp  38980  lshpnel2N  38986  lshpset2N  39120  dicffval  41176  dicfval  41177  mapdhval  41726  hdmap1fval  41798  hdmap1vallem  41799  hdmap1val  41800  aks6d1c6isolem1  42175  aks6d1c6lem5  42178  diophin  42783  eldioph4b  42822  eldioph4i  42823  diophren  42824  fperiodmullem  45315  fargshiftfva  47430  paireqne  47498  isuspgrim0  47872  grimidvtxedg  47876  grimcnv  47879  grimco  47880  uhgrimisgrgriclem  47898  clnbgrgrimlem  47901