Theorem fveqeq2d 6875

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529

This theorem is referenced by:  fveqeq2  6876  op1stg  7982  op2ndg  7983  ttrclss  9675  ttrclselem2  9681  fpwwecbv  10602  fpwwelem  10603  fseq1m1p1  13604  ico01fl0  13829  divfl0  13834  hashssdif  14425  cshw1  14835  smumullem  16526  algcvga  16613  vdwlem6  17022  vdwlem8  17024  ramub1lem1  17062  resmgmhm  18745  resmhm  18854  fislw  19665  pgpfaclem2  20124  0ringdif  20577  abvfval  20859  abvpropd  20884  lspsneq0  21079  reslmhm  21119  lspsneq  21192  mdetunilem7  22678  imasdsf1olem  24433  bcth  25391  ovoliunnul  25569  lognegb  26655  vmaval  27177  2lgslem3c  27462  2lgslem3d  27463  rusgrnumwrdl2  29787  wlkiswwlks2  30075  rusgrnumwwlks  30177  clwlkclwwlklem1  30201  clwlkclwwlklem2  30202  numclwwlk1  30563  wlkl0  30569  numclwlk1lem1  30571  isnvlem  30813  lnoval  30955  normsub0  31339  elunop2  32216  ishst  32417  hstri  32468  aciunf1lem  32864  esplyfvaln  33871  esplyind  33872  vietadeg1  33875  lmatfval  34111  lmatcl  34113  voliune  34526  volfiniune  34527  snmlval  35681  qdiff  37819  voliunnfl  38163  sdclem1  38242  islshp  39603  lshpnel2N  39609  lshpset2N  39743  dicffval  41798  dicfval  41799  mapdhval  42348  hdmap1fval  42420  hdmap1vallem  42421  hdmap1val  42422  aks6d1c6isolem1  42791  aks6d1c6lem5  42794  diophin  43353  eldioph4b  43388  eldioph4i  43389  diophren  43390  fperiodmullem  45882  fourierdlem48  46728  fourierdlem49  46729  fargshiftfva  48049  paireqne  48117  grimidvtxedg  48507  grimcnv  48510  grimco  48511  isuspgrim0  48516  uhgrimisgrgriclem  48552  clnbgrgrimlem  48555