Theorem fveqeq2d 6840

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498

This theorem is referenced by:  fveqeq2  6841  op1stg  7943  op2ndg  7944  ttrclss  9627  ttrclselem2  9633  fpwwecbv  10553  fpwwelem  10554  fseq1m1p1  13513  ico01fl0  13737  divfl0  13742  hashssdif  14333  cshw1  14743  smumullem  16417  algcvga  16504  vdwlem6  16912  vdwlem8  16914  ramub1lem1  16952  resmgmhm  18634  resmhm  18743  isghmOLD  19143  fislw  19552  pgpfaclem2  20011  0ringdif  20458  abvfval  20741  abvpropd  20766  lspsneq0  20961  reslmhm  21002  lspsneq  21075  mdetunilem7  22560  imasdsf1olem  24315  bcth  25283  ovoliunnul  25462  lognegb  26553  vmaval  27077  2lgslem3c  27363  2lgslem3d  27364  rusgrnumwrdl2  29609  wlkiswwlks2  29897  rusgrnumwwlks  29999  clwlkclwwlklem1  30023  clwlkclwwlklem2  30024  numclwwlk1  30385  wlkl0  30391  numclwlk1lem1  30393  isnvlem  30634  lnoval  30776  normsub0  31160  elunop2  32037  ishst  32238  hstri  32289  aciunf1lem  32689  esplyind  33680  vietadeg1  33683  lmatfval  33920  lmatcl  33922  voliune  34335  volfiniune  34336  snmlval  35474  voliunnfl  37804  sdclem1  37883  islshp  39178  lshpnel2N  39184  lshpset2N  39318  dicffval  41373  dicfval  41374  mapdhval  41923  hdmap1fval  41995  hdmap1vallem  41996  hdmap1val  41997  aks6d1c6isolem1  42367  aks6d1c6lem5  42370  diophin  42956  eldioph4b  42995  eldioph4i  42996  diophren  42997  fperiodmullem  45493  fargshiftfva  47631  paireqne  47699  grimidvtxedg  48073  grimcnv  48076  grimco  48077  isuspgrim0  48082  uhgrimisgrgriclem  48118  clnbgrgrimlem  48121