Theorem fveqeq2d 6866

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

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

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519

This theorem is referenced by:  fveqeq2  6867  op1stg  7980  op2ndg  7981  ttrclss  9673  ttrclselem2  9679  fpwwecbv  10597  fpwwelem  10598  fseq1m1p1  13560  ico01fl0  13781  divfl0  13786  hashssdif  14377  cshw1  14787  smumullem  16462  algcvga  16549  vdwlem6  16957  vdwlem8  16959  ramub1lem1  16997  resmgmhm  18638  resmhm  18747  isghmOLD  19148  fislw  19555  pgpfaclem2  20014  0ringdif  20436  abvfval  20719  abvpropd  20744  lspsneq0  20918  reslmhm  20959  lspsneq  21032  mdetunilem7  22505  imasdsf1olem  24261  bcth  25229  ovoliunnul  25408  lognegb  26499  vmaval  27023  2lgslem3c  27309  2lgslem3d  27310  rusgrnumwrdl2  29514  wlkiswwlks2  29805  rusgrnumwwlks  29904  clwlkclwwlklem1  29928  clwlkclwwlklem2  29929  numclwwlk1  30290  wlkl0  30296  numclwlk1lem1  30298  isnvlem  30539  lnoval  30681  normsub0  31065  elunop2  31942  ishst  32143  hstri  32194  aciunf1lem  32586  lmatfval  33804  lmatcl  33806  voliune  34219  volfiniune  34220  snmlval  35318  voliunnfl  37658  sdclem1  37737  islshp  38972  lshpnel2N  38978  lshpset2N  39112  dicffval  41168  dicfval  41169  mapdhval  41718  hdmap1fval  41790  hdmap1vallem  41791  hdmap1val  41792  aks6d1c6isolem1  42162  aks6d1c6lem5  42165  diophin  42760  eldioph4b  42799  eldioph4i  42800  diophren  42801  fperiodmullem  45301  fargshiftfva  47444  paireqne  47512  grimidvtxedg  47885  grimcnv  47888  grimco  47889  isuspgrim0  47894  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933