Theorem fveqeq2d 6848

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506

This theorem is referenced by:  fveqeq2  6849  op1stg  7954  op2ndg  7955  ttrclss  9641  ttrclselem2  9647  fpwwecbv  10567  fpwwelem  10568  fseq1m1p1  13553  ico01fl0  13778  divfl0  13783  hashssdif  14374  cshw1  14784  smumullem  16461  algcvga  16548  vdwlem6  16957  vdwlem8  16959  ramub1lem1  16997  resmgmhm  18679  resmhm  18788  isghmOLD  19191  fislw  19600  pgpfaclem2  20059  0ringdif  20504  abvfval  20787  abvpropd  20812  lspsneq0  21007  reslmhm  21047  lspsneq  21120  mdetunilem7  22583  imasdsf1olem  24338  bcth  25296  ovoliunnul  25474  lognegb  26554  vmaval  27076  2lgslem3c  27361  2lgslem3d  27362  rusgrnumwrdl2  29655  wlkiswwlks2  29943  rusgrnumwwlks  30045  clwlkclwwlklem1  30069  clwlkclwwlklem2  30070  numclwwlk1  30431  wlkl0  30437  numclwlk1lem1  30439  isnvlem  30681  lnoval  30823  normsub0  31207  elunop2  32084  ishst  32285  hstri  32336  aciunf1lem  32735  esplyfvaln  33718  esplyind  33719  vietadeg1  33722  lmatfval  33958  lmatcl  33960  voliune  34373  volfiniune  34374  snmlval  35513  qdiff  37641  voliunnfl  37985  sdclem1  38064  islshp  39425  lshpnel2N  39431  lshpset2N  39565  dicffval  41620  dicfval  41621  mapdhval  42170  hdmap1fval  42242  hdmap1vallem  42243  hdmap1val  42244  aks6d1c6isolem1  42613  aks6d1c6lem5  42616  diophin  43204  eldioph4b  43239  eldioph4i  43240  diophren  43241  fperiodmullem  45736  fargshiftfva  47903  paireqne  47971  grimidvtxedg  48361  grimcnv  48364  grimco  48365  isuspgrim0  48370  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409