Theorem fveqeq2d 6884

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539

This theorem is referenced by:  fveqeq2  6885  op1stg  8000  op2ndg  8001  ttrclss  9734  ttrclselem2  9740  fpwwecbv  10658  fpwwelem  10659  fseq1m1p1  13616  ico01fl0  13836  divfl0  13841  hashssdif  14430  cshw1  14840  smumullem  16511  algcvga  16598  vdwlem6  17006  vdwlem8  17008  ramub1lem1  17046  resmgmhm  18689  resmhm  18798  isghmOLD  19199  fislw  19606  pgpfaclem2  20065  0ringdif  20487  abvfval  20770  abvpropd  20795  lspsneq0  20969  reslmhm  21010  lspsneq  21083  mdetunilem7  22556  imasdsf1olem  24312  bcth  25281  ovoliunnul  25460  lognegb  26551  vmaval  27075  2lgslem3c  27361  2lgslem3d  27362  rusgrnumwrdl2  29566  wlkiswwlks2  29857  rusgrnumwwlks  29956  clwlkclwwlklem1  29980  clwlkclwwlklem2  29981  numclwwlk1  30342  wlkl0  30348  numclwlk1lem1  30350  isnvlem  30591  lnoval  30733  normsub0  31117  elunop2  31994  ishst  32195  hstri  32246  aciunf1lem  32640  lmatfval  33845  lmatcl  33847  voliune  34260  volfiniune  34261  snmlval  35353  voliunnfl  37688  sdclem1  37767  islshp  38997  lshpnel2N  39003  lshpset2N  39137  dicffval  41193  dicfval  41194  mapdhval  41743  hdmap1fval  41815  hdmap1vallem  41816  hdmap1val  41817  aks6d1c6isolem1  42187  aks6d1c6lem5  42190  diophin  42795  eldioph4b  42834  eldioph4i  42835  diophren  42836  fperiodmullem  45332  fargshiftfva  47457  paireqne  47525  grimidvtxedg  47898  grimcnv  47901  grimco  47902  isuspgrim0  47907  uhgrimisgrgriclem  47943  clnbgrgrimlem  47946