Theorem fveqeq2d 6769

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

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

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 2109  ax-9 2117  ax-ext 2708

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 2715  df-cleq 2729  df-clel 2815  df-rab 3071  df-v 3429  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-iota 6381  df-fv 6431

This theorem is referenced by:  fveqeq2  6770  op1stg  7821  op2ndg  7822  fpwwecbv  10347  fpwwelem  10348  fseq1m1p1  13276  ico01fl0  13483  divfl0  13488  hashssdif  14071  cshw1  14479  smumullem  16143  algcvga  16228  vdwlem6  16631  vdwlem8  16633  ramub1lem1  16671  resmhm  18403  isghm  18778  fislw  19174  pgpfaclem2  19629  abvfval  20022  abvpropd  20046  lspsneq0  20218  reslmhm  20258  lspsneq  20328  mdetunilem7  21711  imasdsf1olem  23470  bcth  24436  ovoliunnul  24614  lognegb  25688  vmaval  26205  2lgslem3c  26489  2lgslem3d  26490  rusgrnumwrdl2  27896  wlkiswwlks2  28181  rusgrnumwwlks  28280  clwlkclwwlklem1  28304  clwlkclwwlklem2  28305  numclwwlk1  28666  wlkl0  28672  numclwlk1lem1  28674  isnvlem  28913  lnoval  29055  normsub0  29439  elunop2  30316  ishst  30517  hstri  30568  aciunf1lem  30941  lmatfval  31706  lmatcl  31708  voliune  32139  volfiniune  32140  snmlval  33235  ttrclss  33748  ttrclselem2  33754  voliunnfl  35790  sdclem1  35870  islshp  36962  lshpnel2N  36968  lshpset2N  37102  dicffval  39157  dicfval  39158  mapdhval  39707  hdmap1fval  39779  hdmap1vallem  39780  hdmap1val  39781  diophin  40552  eldioph4b  40591  eldioph4i  40592  diophren  40593  fperiodmullem  42774  fargshiftfva  44825  paireqne  44893  resmgmhm  45282  0ringdif  45358