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

Theorem fvmpts 6826
Description: Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
fvmpts.1 𝐹 = (𝑥𝐶𝐵)
Assertion
Ref Expression
fvmpts ((𝐴𝐶𝐴 / 𝑥𝐵𝑉) → (𝐹𝐴) = 𝐴 / 𝑥𝐵)
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmpts
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 csbeq1 3819 . 2 (𝑦 = 𝐴𝑦 / 𝑥𝐵 = 𝐴 / 𝑥𝐵)
2 fvmpts.1 . . 3 𝐹 = (𝑥𝐶𝐵)
3 nfcv 2904 . . . 4 𝑦𝐵
4 nfcsb1v 3841 . . . 4 𝑥𝑦 / 𝑥𝐵
5 csbeq1a 3830 . . . 4 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
63, 4, 5cbvmpt 5161 . . 3 (𝑥𝐶𝐵) = (𝑦𝐶𝑦 / 𝑥𝐵)
72, 6eqtri 2765 . 2 𝐹 = (𝑦𝐶𝑦 / 𝑥𝐵)
81, 7fvmptg 6821 1 ((𝐴𝐶𝐴 / 𝑥𝐵𝑉) → (𝐹𝐴) = 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2110  csb 3816  cmpt 5140  cfv 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pr 5327
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-br 5059  df-opab 5121  df-mpt 5141  df-id 5460  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-iota 6343  df-fun 6387  df-fv 6393
This theorem is referenced by:  fvmptdf  6829  fvmpocurryd  8018  mptnn0fsupp  13575  mptnn0fsuppr  13577  zsum  15287  prodss  15514  fprodser  15516  fprodn0  15546  fprodefsum  15661  pcmpt  16450  issubc  17346  gsummptnn0fz  19376  mptscmfsupp0  19969  gsummoncoe1  21230  fvmptnn04if  21751  prdsdsf  23270  itgparts  24949  dchrisumlema  26374  abfmpeld  30716  abfmpel  30717  cdlemk40  38673  aomclem6  40595  ellimcabssub0  42841  constlimc  42848  vonn0ioo2  43911  vonn0icc2  43913
  Copyright terms: Public domain W3C validator