Theorem fveqeq2d 6791

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445

This theorem is referenced by:  fveqeq2  6792  op1stg  7852  op2ndg  7853  ttrclss  9487  ttrclselem2  9493  fpwwecbv  10409  fpwwelem  10410  fseq1m1p1  13340  ico01fl0  13548  divfl0  13553  hashssdif  14136  cshw1  14544  smumullem  16208  algcvga  16293  vdwlem6  16696  vdwlem8  16698  ramub1lem1  16736  resmhm  18468  isghm  18843  fislw  19239  pgpfaclem2  19694  abvfval  20087  abvpropd  20111  lspsneq0  20283  reslmhm  20323  lspsneq  20393  mdetunilem7  21776  imasdsf1olem  23535  bcth  24502  ovoliunnul  24680  lognegb  25754  vmaval  26271  2lgslem3c  26555  2lgslem3d  26556  rusgrnumwrdl2  27962  wlkiswwlks2  28249  rusgrnumwwlks  28348  clwlkclwwlklem1  28372  clwlkclwwlklem2  28373  numclwwlk1  28734  wlkl0  28740  numclwlk1lem1  28742  isnvlem  28981  lnoval  29123  normsub0  29507  elunop2  30384  ishst  30585  hstri  30636  aciunf1lem  31008  lmatfval  31773  lmatcl  31775  voliune  32206  volfiniune  32207  snmlval  33302  voliunnfl  35830  sdclem1  35910  islshp  37000  lshpnel2N  37006  lshpset2N  37140  dicffval  39195  dicfval  39196  mapdhval  39745  hdmap1fval  39817  hdmap1vallem  39818  hdmap1val  39819  diophin  40601  eldioph4b  40640  eldioph4i  40641  diophren  40642  fperiodmullem  42849  fargshiftfva  44906  paireqne  44974  resmgmhm  45363  0ringdif  45439