Theorem fveqeq2d 6850

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508

This theorem is referenced by:  fveqeq2  6851  op1stg  7955  op2ndg  7956  ttrclss  9641  ttrclselem2  9647  fpwwecbv  10567  fpwwelem  10568  fseq1m1p1  13527  ico01fl0  13751  divfl0  13756  hashssdif  14347  cshw1  14757  smumullem  16431  algcvga  16518  vdwlem6  16926  vdwlem8  16928  ramub1lem1  16966  resmgmhm  18648  resmhm  18757  isghmOLD  19160  fislw  19569  pgpfaclem2  20028  0ringdif  20475  abvfval  20758  abvpropd  20783  lspsneq0  20978  reslmhm  21019  lspsneq  21092  mdetunilem7  22577  imasdsf1olem  24332  bcth  25300  ovoliunnul  25479  lognegb  26570  vmaval  27094  2lgslem3c  27380  2lgslem3d  27381  rusgrnumwrdl2  29676  wlkiswwlks2  29964  rusgrnumwwlks  30066  clwlkclwwlklem1  30090  clwlkclwwlklem2  30091  numclwwlk1  30452  wlkl0  30458  numclwlk1lem1  30460  isnvlem  30702  lnoval  30844  normsub0  31228  elunop2  32105  ishst  32306  hstri  32357  aciunf1lem  32756  esplyfvaln  33755  esplyind  33756  vietadeg1  33759  lmatfval  33996  lmatcl  33998  voliune  34411  volfiniune  34412  snmlval  35551  voliunnfl  37919  sdclem1  37998  islshp  39359  lshpnel2N  39365  lshpset2N  39499  dicffval  41554  dicfval  41555  mapdhval  42104  hdmap1fval  42176  hdmap1vallem  42177  hdmap1val  42178  aks6d1c6isolem1  42548  aks6d1c6lem5  42551  diophin  43133  eldioph4b  43172  eldioph4i  43173  diophren  43174  fperiodmullem  45669  fargshiftfva  47807  paireqne  47875  grimidvtxedg  48249  grimcnv  48252  grimco  48253  isuspgrim0  48258  uhgrimisgrgriclem  48294  clnbgrgrimlem  48297