Theorem fveqeq2d 6899

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551

This theorem is referenced by:  fveqeq2  6900  op1stg  7986  op2ndg  7987  ttrclss  9714  ttrclselem2  9720  fpwwecbv  10638  fpwwelem  10639  fseq1m1p1  13575  ico01fl0  13783  divfl0  13788  hashssdif  14371  cshw1  14771  smumullem  16432  algcvga  16515  vdwlem6  16918  vdwlem8  16920  ramub1lem1  16958  resmhm  18700  isghm  19091  fislw  19492  pgpfaclem2  19951  abvfval  20425  abvpropd  20449  lspsneq0  20622  reslmhm  20662  lspsneq  20734  mdetunilem7  22119  imasdsf1olem  23878  bcth  24845  ovoliunnul  25023  lognegb  26097  vmaval  26614  2lgslem3c  26898  2lgslem3d  26899  rusgrnumwrdl2  28840  wlkiswwlks2  29126  rusgrnumwwlks  29225  clwlkclwwlklem1  29249  clwlkclwwlklem2  29250  numclwwlk1  29611  wlkl0  29617  numclwlk1lem1  29619  isnvlem  29858  lnoval  30000  normsub0  30384  elunop2  31261  ishst  31462  hstri  31513  aciunf1lem  31882  lmatfval  32789  lmatcl  32791  voliune  33222  volfiniune  33223  snmlval  34317  voliunnfl  36527  sdclem1  36606  islshp  37844  lshpnel2N  37850  lshpset2N  37984  dicffval  40040  dicfval  40041  mapdhval  40590  hdmap1fval  40662  hdmap1vallem  40663  hdmap1val  40664  diophin  41500  eldioph4b  41539  eldioph4i  41540  diophren  41541  fperiodmullem  44003  fargshiftfva  46101  paireqne  46169  resmgmhm  46558  0ringdif  46634