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 2733	1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

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

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  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  7991  op2ndg  7992  ttrclss  9721  ttrclselem2  9727  fpwwecbv  10645  fpwwelem  10646  fseq1m1p1  13583  ico01fl0  13791  divfl0  13796  hashssdif  14379  cshw1  14779  smumullem  16440  algcvga  16523  vdwlem6  16926  vdwlem8  16928  ramub1lem1  16966  resmgmhm  18642  resmhm  18743  isghm  19137  fislw  19541  pgpfaclem2  20000  0ringdif  20423  abvfval  20657  abvpropd  20681  lspsneq0  20855  reslmhm  20896  lspsneq  20969  mdetunilem7  22441  imasdsf1olem  24200  bcth  25178  ovoliunnul  25357  lognegb  26439  vmaval  26960  2lgslem3c  27246  2lgslem3d  27247  rusgrnumwrdl2  29278  wlkiswwlks2  29564  rusgrnumwwlks  29663  clwlkclwwlklem1  29687  clwlkclwwlklem2  29688  numclwwlk1  30049  wlkl0  30055  numclwlk1lem1  30057  isnvlem  30298  lnoval  30440  normsub0  30824  elunop2  31701  ishst  31902  hstri  31953  aciunf1lem  32322  lmatfval  33260  lmatcl  33262  voliune  33693  volfiniune  33694  snmlval  34788  voliunnfl  36999  sdclem1  37078  islshp  38316  lshpnel2N  38322  lshpset2N  38456  dicffval  40512  dicfval  40513  mapdhval  41062  hdmap1fval  41134  hdmap1vallem  41135  hdmap1val  41136  diophin  41976  eldioph4b  42015  eldioph4i  42016  diophren  42017  fperiodmullem  44475  fargshiftfva  46573  paireqne  46641