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

Theorem fveqeq2d 6675
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 6671 . 2 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
32eqeq1d 2828 1 (𝜑 → ((𝐹𝐴) = 𝐶 ↔ (𝐹𝐵) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  cfv 6352
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6312  df-fv 6360
This theorem is referenced by:  fveqeq2  6676  op1stg  7692  op2ndg  7693  fpwwecbv  10055  fpwwelem  10056  fseq1m1p1  12972  ico01fl0  13179  divfl0  13184  hashssdif  13763  cshw1  14174  smumullem  15831  algcvga  15913  vdwlem6  16312  vdwlem8  16314  ramub1lem1  16352  resmhm  17968  isghm  18288  fislw  18670  pgpfaclem2  19124  abvfval  19509  abvpropd  19533  lspsneq0  19704  reslmhm  19744  lspsneq  19814  mdetunilem7  21143  imasdsf1olem  22898  bcth  23847  ovoliunnul  24023  lognegb  25086  vmaval  25604  2lgslem3c  25888  2lgslem3d  25889  rusgrnumwrdl2  27282  wlkiswwlks2  27567  rusgrnumwwlks  27667  clwlkclwwlklem1  27691  clwlkclwwlklem2  27692  numclwwlk1  28054  wlkl0  28060  numclwlk1lem1  28062  isnvlem  28301  lnoval  28443  normsub0  28827  elunop2  29704  ishst  29905  hstri  29956  aciunf1lem  30322  lmatfval  30965  lmatcl  30967  voliune  31374  volfiniune  31375  snmlval  32462  voliunnfl  34803  sdclem1  34886  islshp  35982  lshpnel2N  35988  lshpset2N  36122  dicffval  38177  dicfval  38178  mapdhval  38727  hdmap1fval  38799  hdmap1vallem  38800  hdmap1val  38801  diophin  39234  eldioph4b  39273  eldioph4i  39274  diophren  39275  fperiodmullem  41435  fargshiftfva  43435  paireqne  43505  resmgmhm  43897  0ringdif  43973
  Copyright terms: Public domain W3C validator