Theorem fveqeq2d 6830

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ‘cfv 6481

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489

This theorem is referenced by:  fveqeq2  6831  op1stg  7933  op2ndg  7934  ttrclss  9610  ttrclselem2  9616  fpwwecbv  10535  fpwwelem  10536  fseq1m1p1  13499  ico01fl0  13723  divfl0  13728  hashssdif  14319  cshw1  14729  smumullem  16403  algcvga  16490  vdwlem6  16898  vdwlem8  16900  ramub1lem1  16938  resmgmhm  18619  resmhm  18728  isghmOLD  19128  fislw  19537  pgpfaclem2  19996  0ringdif  20442  abvfval  20725  abvpropd  20750  lspsneq0  20945  reslmhm  20986  lspsneq  21059  mdetunilem7  22533  imasdsf1olem  24288  bcth  25256  ovoliunnul  25435  lognegb  26526  vmaval  27050  2lgslem3c  27336  2lgslem3d  27337  rusgrnumwrdl2  29565  wlkiswwlks2  29853  rusgrnumwwlks  29955  clwlkclwwlklem1  29979  clwlkclwwlklem2  29980  numclwwlk1  30341  wlkl0  30347  numclwlk1lem1  30349  isnvlem  30590  lnoval  30732  normsub0  31116  elunop2  31993  ishst  32194  hstri  32245  aciunf1lem  32644  lmatfval  33827  lmatcl  33829  voliune  34242  volfiniune  34243  snmlval  35375  voliunnfl  37714  sdclem1  37793  islshp  39088  lshpnel2N  39094  lshpset2N  39228  dicffval  41283  dicfval  41284  mapdhval  41833  hdmap1fval  41905  hdmap1vallem  41906  hdmap1val  41907  aks6d1c6isolem1  42277  aks6d1c6lem5  42280  diophin  42875  eldioph4b  42914  eldioph4i  42915  diophren  42916  fperiodmullem  45414  fargshiftfva  47553  paireqne  47621  grimidvtxedg  47995  grimcnv  47998  grimco  47999  isuspgrim0  48004  uhgrimisgrgriclem  48040  clnbgrgrimlem  48043