Theorem fveqeq2d 6890

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545

This theorem is referenced by:  fveqeq2  6891  op1stg  7998  op2ndg  7999  ttrclss  9689  ttrclselem2  9695  fpwwecbv  10629  fpwwelem  10630  fseq1m1p1  13627  ico01fl0  13852  divfl0  13857  hashssdif  14449  cshw1  14859  smumullem  16550  algcvga  16637  vdwlem6  17046  vdwlem8  17048  ramub1lem1  17086  resmgmhm  18769  resmhm  18879  fislw  19695  pgpfaclem2  20154  0ringdif  20611  abvfval  20891  abvpropd  20916  lspsneq0  21111  reslmhm  21151  lspsneq  21224  mdetunilem7  22744  imasdsf1olem  24499  bcth  25457  ovoliunnul  25635  lognegb  26721  vmaval  27243  2lgslem3c  27528  2lgslem3d  27529  rusgrnumwrdl2  29877  wlkiswwlks2  30165  rusgrnumwwlks  30267  clwlkclwwlklem1  30291  clwlkclwwlklem2  30292  numclwwlk1  30653  wlkl0  30659  numclwlk1lem1  30661  isnvlem  30903  lnoval  31045  normsub0  31429  elunop2  32306  ishst  32507  hstri  32558  aciunf1lem  32948  esplyfvaln  33909  esplyind  33910  vietadeg1  33913  lmatfval  34149  lmatcl  34151  voliune  34564  volfiniune  34565  snmlval  35756  qdiff  37893  voliunnfl  38237  sdclem1  38316  islshp  39677  lshpnel2N  39683  lshpset2N  39817  dicffval  41872  dicfval  41873  mapdhval  42422  hdmap1fval  42494  hdmap1vallem  42495  hdmap1val  42496  aks6d1c6isolem1  42865  aks6d1c6lem5  42868  diophin  43429  eldioph4b  43464  eldioph4i  43465  diophren  43466  fperiodmullem  45948  fourierdlem48  46794  fourierdlem49  46795  fargshiftfva  48115  paireqne  48183  grimidvtxedg  48573  grimcnv  48576  grimco  48577  isuspgrim0  48582  uhgrimisgrgriclem  48618  clnbgrgrimlem  48621