Theorem fveqeq2d 6843

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ‘cfv 6493

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501

This theorem is referenced by:  fveqeq2  6844  op1stg  7948  op2ndg  7949  ttrclss  9635  ttrclselem2  9641  fpwwecbv  10561  fpwwelem  10562  fseq1m1p1  13547  ico01fl0  13772  divfl0  13777  hashssdif  14368  cshw1  14778  smumullem  16455  algcvga  16542  vdwlem6  16951  vdwlem8  16953  ramub1lem1  16991  resmgmhm  18673  resmhm  18782  isghmOLD  19185  fislw  19594  pgpfaclem2  20053  0ringdif  20498  abvfval  20781  abvpropd  20806  lspsneq0  21001  reslmhm  21042  lspsneq  21115  mdetunilem7  22596  imasdsf1olem  24351  bcth  25309  ovoliunnul  25487  lognegb  26570  vmaval  27093  2lgslem3c  27378  2lgslem3d  27379  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  32753  esplyfvaln  33736  esplyind  33737  vietadeg1  33740  lmatfval  33977  lmatcl  33979  voliune  34392  volfiniune  34393  snmlval  35532  voliunnfl  38002  sdclem1  38081  islshp  39442  lshpnel2N  39448  lshpset2N  39582  dicffval  41637  dicfval  41638  mapdhval  42187  hdmap1fval  42259  hdmap1vallem  42260  hdmap1val  42261  aks6d1c6isolem1  42630  aks6d1c6lem5  42633  diophin  43221  eldioph4b  43260  eldioph4i  43261  diophren  43262  fperiodmullem  45757  fargshiftfva  47918  paireqne  47986  grimidvtxedg  48376  grimcnv  48379  grimco  48380  isuspgrim0  48385  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424