Theorem fveqeq2d 6835

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493

This theorem is referenced by:  fveqeq2  6836  op1stg  7943  op2ndg  7944  ttrclss  9632  ttrclselem2  9638  fpwwecbv  10558  fpwwelem  10559  fseq1m1p1  13544  ico01fl0  13769  divfl0  13774  hashssdif  14365  cshw1  14775  smumullem  16452  algcvga  16539  vdwlem6  16948  vdwlem8  16950  ramub1lem1  16988  resmgmhm  18670  resmhm  18779  isghmOLD  19182  fislw  19591  pgpfaclem2  20050  0ringdif  20499  abvfval  20782  abvpropd  20807  lspsneq0  21002  reslmhm  21042  lspsneq  21115  mdetunilem7  22601  imasdsf1olem  24356  bcth  25314  ovoliunnul  25492  lognegb  26572  vmaval  27094  2lgslem3c  27379  2lgslem3d  27380  rusgrnumwrdl2  29673  wlkiswwlks2  29961  rusgrnumwwlks  30063  clwlkclwwlklem1  30087  clwlkclwwlklem2  30088  numclwwlk1  30449  wlkl0  30455  numclwlk1lem1  30457  isnvlem  30699  lnoval  30841  normsub0  31225  elunop2  32102  ishst  32303  hstri  32354  aciunf1lem  32754  esplyfvaln  33758  esplyind  33759  vietadeg1  33762  lmatfval  33998  lmatcl  34000  voliune  34413  volfiniune  34414  snmlval  35559  qdiff  37687  voliunnfl  38031  sdclem1  38110  islshp  39471  lshpnel2N  39477  lshpset2N  39611  dicffval  41666  dicfval  41667  mapdhval  42216  hdmap1fval  42288  hdmap1vallem  42289  hdmap1val  42290  aks6d1c6isolem1  42659  aks6d1c6lem5  42662  diophin  43221  eldioph4b  43256  eldioph4i  43257  diophren  43258  fperiodmullem  45751  fargshiftfva  47918  paireqne  47986  grimidvtxedg  48376  grimcnv  48379  grimco  48380  isuspgrim0  48385  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424