Theorem fveqeq2d 6842

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500

This theorem is referenced by:  fveqeq2  6843  op1stg  7945  op2ndg  7946  ttrclss  9631  ttrclselem2  9637  fpwwecbv  10557  fpwwelem  10558  fseq1m1p1  13517  ico01fl0  13741  divfl0  13746  hashssdif  14337  cshw1  14747  smumullem  16421  algcvga  16508  vdwlem6  16916  vdwlem8  16918  ramub1lem1  16956  resmgmhm  18638  resmhm  18747  isghmOLD  19147  fislw  19556  pgpfaclem2  20015  0ringdif  20462  abvfval  20745  abvpropd  20770  lspsneq0  20965  reslmhm  21006  lspsneq  21079  mdetunilem7  22564  imasdsf1olem  24319  bcth  25287  ovoliunnul  25466  lognegb  26557  vmaval  27081  2lgslem3c  27367  2lgslem3d  27368  rusgrnumwrdl2  29662  wlkiswwlks2  29950  rusgrnumwwlks  30052  clwlkclwwlklem1  30076  clwlkclwwlklem2  30077  numclwwlk1  30438  wlkl0  30444  numclwlk1lem1  30446  isnvlem  30687  lnoval  30829  normsub0  31213  elunop2  32090  ishst  32291  hstri  32342  aciunf1lem  32742  esplyind  33733  vietadeg1  33736  lmatfval  33973  lmatcl  33975  voliune  34388  volfiniune  34389  snmlval  35527  voliunnfl  37867  sdclem1  37946  islshp  39261  lshpnel2N  39267  lshpset2N  39401  dicffval  41456  dicfval  41457  mapdhval  42006  hdmap1fval  42078  hdmap1vallem  42079  hdmap1val  42080  aks6d1c6isolem1  42450  aks6d1c6lem5  42453  diophin  43035  eldioph4b  43074  eldioph4i  43075  diophren  43076  fperiodmullem  45572  fargshiftfva  47710  paireqne  47778  grimidvtxedg  48152  grimcnv  48155  grimco  48156  isuspgrim0  48161  uhgrimisgrgriclem  48197  clnbgrgrimlem  48200