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

Theorem fveqeq2d 6855
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 6851 . 2 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
32eqeq1d 2739 1 (𝜑 → ((𝐹𝐴) = 𝐶 ↔ (𝐹𝐵) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  cfv 6501
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509
This theorem is referenced by:  fveqeq2  6856  op1stg  7938  op2ndg  7939  ttrclss  9663  ttrclselem2  9669  fpwwecbv  10587  fpwwelem  10588  fseq1m1p1  13523  ico01fl0  13731  divfl0  13736  hashssdif  14319  cshw1  14717  smumullem  16379  algcvga  16462  vdwlem6  16865  vdwlem8  16867  ramub1lem1  16905  resmhm  18638  isghm  19015  fislw  19414  pgpfaclem2  19868  abvfval  20293  abvpropd  20317  lspsneq0  20489  reslmhm  20529  lspsneq  20599  mdetunilem7  21983  imasdsf1olem  23742  bcth  24709  ovoliunnul  24887  lognegb  25961  vmaval  26478  2lgslem3c  26762  2lgslem3d  26763  rusgrnumwrdl2  28576  wlkiswwlks2  28862  rusgrnumwwlks  28961  clwlkclwwlklem1  28985  clwlkclwwlklem2  28986  numclwwlk1  29347  wlkl0  29353  numclwlk1lem1  29355  isnvlem  29594  lnoval  29736  normsub0  30120  elunop2  30997  ishst  31198  hstri  31249  aciunf1lem  31620  lmatfval  32435  lmatcl  32437  voliune  32868  volfiniune  32869  snmlval  33965  voliunnfl  36151  sdclem1  36231  islshp  37470  lshpnel2N  37476  lshpset2N  37610  dicffval  39666  dicfval  39667  mapdhval  40216  hdmap1fval  40288  hdmap1vallem  40289  hdmap1val  40290  diophin  41124  eldioph4b  41163  eldioph4i  41164  diophren  41165  fperiodmullem  43611  fargshiftfva  45709  paireqne  45777  resmgmhm  46166  0ringdif  46242
  Copyright terms: Public domain W3C validator