Theorem fveqeq2d 6893

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548

This theorem is used by:  fveqeq2  6894  op1stg  8004  op2ndg  8005  ttrclss  9696  ttrclselem2  9702  fpwwecbv  10646  fpwwelem  10647  fseq1m1p1  13646  ico01fl0  13872  divfl0  13877  hashssdif  14469  cshw1  14885  smumullem  16574  algcvga  16661  vdwlem6  17070  vdwlem8  17072  ramub1lem1  17110  resmgmhm  18803  resmhm  18918  fislw  19741  pgpfaclem2  20200  0ringdif  20677  abvfval  20965  abvpropd  20990  lspsneq0  21185  reslmhm  21225  lspsneq  21298  mdetunilem7  22827  imasdsf1olem  24583  bcth  25541  ovoliunnul  25719  lognegb  26808  vmaval  27330  2lgslem3c  27615  2lgslem3d  27616  rusgrnumwrdl2  29996  wlkiswwlks2  30293  rusgrnumwwlks  30395  clwlkclwwlklem1  30419  clwlkclwwlklem2  30420  numclwwlk1  30785  wlkl0  30791  numclwlk1lem1  30793  isnvlem  31035  lnoval  31177  normsub0  31561  elunop2  32438  ishst  32639  hstri  32690  aciunf1lem  33080  esplyfvaln  34030  esplyind  34031  vietadeg1  34034  lmatfval  34270  lmatcl  34272  voliune  34686  volfiniune  34687  snmlval  35862  qdiff  38030  voliunnfl  38374  sdclem1  38454  islshp  39813  lshpnel2N  39819  lshpset2N  39953  dicffval  42008  dicfval  42009  mapdhval  42558  hdmap1fval  42630  hdmap1vallem  42631  hdmap1val  42632  aks6d1c6isolem1  43001  aks6d1c6lem5  43004  diophin  43563  eldioph4b  43598  eldioph4i  43599  diophren  43600  fperiodmullem  46082  fourierdlem48  46928  fourierdlem49  46929  fargshiftfva  48252  paireqne  48320  grimidvtxedg  48710  grimcnv  48713  grimco  48714  isuspgrim0  48719  uhgrimisgrgriclem  48755  clnbgrgrimlem  48758