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 2731	1 ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490

This theorem is referenced by:  fveqeq2  6831  op1stg  7936  op2ndg  7937  ttrclss  9616  ttrclselem2  9622  fpwwecbv  10538  fpwwelem  10539  fseq1m1p1  13502  ico01fl0  13723  divfl0  13728  hashssdif  14319  cshw1  14728  smumullem  16403  algcvga  16490  vdwlem6  16898  vdwlem8  16900  ramub1lem1  16938  resmgmhm  18585  resmhm  18694  isghmOLD  19095  fislw  19504  pgpfaclem2  19963  0ringdif  20412  abvfval  20695  abvpropd  20720  lspsneq0  20915  reslmhm  20956  lspsneq  21029  mdetunilem7  22503  imasdsf1olem  24259  bcth  25227  ovoliunnul  25406  lognegb  26497  vmaval  27021  2lgslem3c  27307  2lgslem3d  27308  rusgrnumwrdl2  29532  wlkiswwlks2  29820  rusgrnumwwlks  29919  clwlkclwwlklem1  29943  clwlkclwwlklem2  29944  numclwwlk1  30305  wlkl0  30311  numclwlk1lem1  30313  isnvlem  30554  lnoval  30696  normsub0  31080  elunop2  31957  ishst  32158  hstri  32209  aciunf1lem  32606  lmatfval  33787  lmatcl  33789  voliune  34202  volfiniune  34203  snmlval  35314  voliunnfl  37654  sdclem1  37733  islshp  38968  lshpnel2N  38974  lshpset2N  39108  dicffval  41163  dicfval  41164  mapdhval  41713  hdmap1fval  41785  hdmap1vallem  41786  hdmap1val  41787  aks6d1c6isolem1  42157  aks6d1c6lem5  42160  diophin  42755  eldioph4b  42794  eldioph4i  42795  diophren  42796  fperiodmullem  45295  fargshiftfva  47437  paireqne  47505  grimidvtxedg  47879  grimcnv  47882  grimco  47883  isuspgrim0  47888  uhgrimisgrgriclem  47924  clnbgrgrimlem  47927