Theorem fveqeq2d 6928

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  fveqeq2  6929  op1stg  8042  op2ndg  8043  ttrclss  9789  ttrclselem2  9795  fpwwecbv  10713  fpwwelem  10714  fseq1m1p1  13659  ico01fl0  13870  divfl0  13875  hashssdif  14461  cshw1  14870  smumullem  16538  algcvga  16626  vdwlem6  17033  vdwlem8  17035  ramub1lem1  17073  resmgmhm  18749  resmhm  18855  isghmOLD  19256  fislw  19667  pgpfaclem2  20126  0ringdif  20553  abvfval  20833  abvpropd  20858  lspsneq0  21033  reslmhm  21074  lspsneq  21147  mdetunilem7  22645  imasdsf1olem  24404  bcth  25382  ovoliunnul  25561  lognegb  26650  vmaval  27174  2lgslem3c  27460  2lgslem3d  27461  rusgrnumwrdl2  29622  wlkiswwlks2  29908  rusgrnumwwlks  30007  clwlkclwwlklem1  30031  clwlkclwwlklem2  30032  numclwwlk1  30393  wlkl0  30399  numclwlk1lem1  30401  isnvlem  30642  lnoval  30784  normsub0  31168  elunop2  32045  ishst  32246  hstri  32297  aciunf1lem  32680  lmatfval  33760  lmatcl  33762  voliune  34193  volfiniune  34194  snmlval  35299  voliunnfl  37624  sdclem1  37703  islshp  38935  lshpnel2N  38941  lshpset2N  39075  dicffval  41131  dicfval  41132  mapdhval  41681  hdmap1fval  41753  hdmap1vallem  41754  hdmap1val  41755  aks6d1c6isolem1  42131  aks6d1c6lem5  42134  diophin  42728  eldioph4b  42767  eldioph4i  42768  diophren  42769  fperiodmullem  45218  fargshiftfva  47317  paireqne  47385  isuspgrim0  47756  grimidvtxedg  47760  grimcnv  47763  grimco  47764  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785