Theorem fveqeq2d 6764

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by:  fveqeq2  6765  op1stg  7816  op2ndg  7817  fpwwecbv  10331  fpwwelem  10332  fseq1m1p1  13260  ico01fl0  13467  divfl0  13472  hashssdif  14055  cshw1  14463  smumullem  16127  algcvga  16212  vdwlem6  16615  vdwlem8  16617  ramub1lem1  16655  resmhm  18374  isghm  18749  fislw  19145  pgpfaclem2  19600  abvfval  19993  abvpropd  20017  lspsneq0  20189  reslmhm  20229  lspsneq  20299  mdetunilem7  21675  imasdsf1olem  23434  bcth  24398  ovoliunnul  24576  lognegb  25650  vmaval  26167  2lgslem3c  26451  2lgslem3d  26452  rusgrnumwrdl2  27856  wlkiswwlks2  28141  rusgrnumwwlks  28240  clwlkclwwlklem1  28264  clwlkclwwlklem2  28265  numclwwlk1  28626  wlkl0  28632  numclwlk1lem1  28634  isnvlem  28873  lnoval  29015  normsub0  29399  elunop2  30276  ishst  30477  hstri  30528  aciunf1lem  30901  lmatfval  31666  lmatcl  31668  voliune  32097  volfiniune  32098  snmlval  33193  ttrclss  33706  ttrclselem2  33712  voliunnfl  35748  sdclem1  35828  islshp  36920  lshpnel2N  36926  lshpset2N  37060  dicffval  39115  dicfval  39116  mapdhval  39665  hdmap1fval  39737  hdmap1vallem  39738  hdmap1val  39739  diophin  40510  eldioph4b  40549  eldioph4i  40550  diophren  40551  fperiodmullem  42732  fargshiftfva  44783  paireqne  44851  resmgmhm  45240  0ringdif  45316