MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fveqeq2d Structured version   Visualization version   GIF version

Theorem fveqeq2d 6910
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
StepHypRef Expression
1 fveqeq2d.1 . . 3 (𝜑𝐴 = 𝐵)
21fveq2d 6906 . 2 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
32eqeq1d 2730 1 (𝜑 → ((𝐹𝐴) = 𝐶 ↔ (𝐹𝐵) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1533  cfv 6553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561
This theorem is referenced by:  fveqeq2  6911  op1stg  8013  op2ndg  8014  ttrclss  9753  ttrclselem2  9759  fpwwecbv  10677  fpwwelem  10678  fseq1m1p1  13618  ico01fl0  13826  divfl0  13831  hashssdif  14413  cshw1  14814  smumullem  16476  algcvga  16559  vdwlem6  16964  vdwlem8  16966  ramub1lem1  17004  resmgmhm  18680  resmhm  18786  isghm  19184  fislw  19594  pgpfaclem2  20053  0ringdif  20478  abvfval  20712  abvpropd  20736  lspsneq0  20910  reslmhm  20951  lspsneq  21024  mdetunilem7  22548  imasdsf1olem  24307  bcth  25285  ovoliunnul  25464  lognegb  26552  vmaval  27073  2lgslem3c  27359  2lgslem3d  27360  rusgrnumwrdl2  29428  wlkiswwlks2  29714  rusgrnumwwlks  29813  clwlkclwwlklem1  29837  clwlkclwwlklem2  29838  numclwwlk1  30199  wlkl0  30205  numclwlk1lem1  30207  isnvlem  30448  lnoval  30590  normsub0  30974  elunop2  31851  ishst  32052  hstri  32103  aciunf1lem  32477  lmatfval  33456  lmatcl  33458  voliune  33889  volfiniune  33890  snmlval  34982  voliunnfl  37178  sdclem1  37257  islshp  38491  lshpnel2N  38497  lshpset2N  38631  dicffval  40687  dicfval  40688  mapdhval  41237  hdmap1fval  41309  hdmap1vallem  41310  hdmap1val  41311  aks6d1c6isolem1  41686  aks6d1c6lem5  41689  diophin  42241  eldioph4b  42280  eldioph4i  42281  diophren  42282  fperiodmullem  44732  fargshiftfva  46830  paireqne  46898  isuspgrim0  47266  grimidvtxedg  47270  grimcnv  47273  grimco  47274
  Copyright terms: Public domain W3C validator