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

Theorem fveqeq2d 6383
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 6379 . 2 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
32eqeq1d 2767 1 (𝜑 → ((𝐹𝐴) = 𝐶 ↔ (𝐹𝐵) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  cfv 6068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076
This theorem is referenced by:  fveqeq2  6384  op1stg  7378  op2ndg  7379  fpwwecbv  9719  fpwwelem  9720  fseq1m1p1  12622  ico01fl0  12828  divfl0  12833  hashssdif  13401  cshw1  13853  smumullem  15497  algcvga  15575  vdwlem6  15971  vdwlem8  15973  ramub1lem1  16011  resmhm  17627  isghm  17926  fislw  18306  pgpfaclem2  18748  abvfval  19087  abvpropd  19111  lspsneq0  19284  reslmhm  19324  lspsneq  19394  mdetunilem7  20701  imasdsf1olem  22457  bcth  23406  ovoliunnul  23565  lognegb  24627  vmaval  25130  2lgslem3c  25414  2lgslem3d  25415  rusgrnumwrdl2  26773  wlkiswwlks2  27065  rusgrnumwwlks  27179  clwlkclwwlklem1  27205  clwlkclwwlklem2  27206  numclwwlk1  27604  wlkl0  27610  numclwlk1lem1  27612  isnvlem  27856  lnoval  27998  normsub0  28384  elunop2  29263  ishst  29464  hstri  29515  aciunf1lem  29847  lmatfval  30262  lmatcl  30264  voliune  30674  volfiniune  30675  snmlval  31693  voliunnfl  33809  sdclem1  33893  islshp  34867  lshpnel2N  34873  lshpset2N  35007  dicffval  37062  dicfval  37063  mapdhval  37612  hdmap1fval  37684  hdmap1vallem  37685  hdmap1val  37686  diophin  37946  eldioph4b  37985  eldioph4i  37986  diophren  37987  fperiodmullem  40088  fargshiftfva  42045  resmgmhm  42399  0ringdif  42471
  Copyright terms: Public domain W3C validator