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

Theorem fvmptd4 6965
Description: Deduction version of fvmpt 6941 (where the substitution hypothesis does not have the antecedent 𝜑). (Contributed by SN, 26-Jul-2024.)
Hypotheses
Ref Expression
fvmptd4.1 (𝑥 = 𝐴𝐵 = 𝐶)
fvmptd4.2 (𝜑𝐹 = (𝑥𝐷𝐵))
fvmptd4.3 (𝜑𝐴𝐷)
fvmptd4.4 (𝜑𝐶𝑉)
Assertion
Ref Expression
fvmptd4 (𝜑 → (𝐹𝐴) = 𝐶)
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd4
StepHypRef Expression
1 fvmptd4.2 . 2 (𝜑𝐹 = (𝑥𝐷𝐵))
2 fvmptd4.1 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
32adantl 481 . 2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
4 fvmptd4.3 . 2 (𝜑𝐴𝐷)
5 fvmptd4.4 . 2 (𝜑𝐶𝑉)
61, 3, 4, 5fvmptd 6948 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2113  cmpt 5179  cfv 6492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500
This theorem is referenced by:  evlsvval  22045  evlsvvval  22048  selvval  22078  mhpmulcl  22092  psdval  22102  psdcoef  22103  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  extvfval  33697  extvfv  33698  extvfvv  33699  evlvarval  33706  mplvrpmrhm  33712  esplyfval  33721  esplyind  33731  vieta  33736  extdgfialglem2  33850  2sqr3minply  33937  cos9thpiminply  33945  evlsvarval  42811  selvvvval  42828  prjcrvval  42875  dvnprodlem1  46190
  Copyright terms: Public domain W3C validator