Theorem fvmpts 6997

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.

Step	Hyp	Ref	Expression
1		csbeq1 3857	. 2 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2		fvmpts.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶 ↦ 𝐵)
3		nfcv 2927	. . . 4 ⊢ Ⅎ𝑦𝐵
4		nfcsb1v 3878	. . . 4 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
5		csbeq1a 3868	. . . 4 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
6	3, 4, 5	cbvmpt 5215	. . 3 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ ⦋𝑦 / 𝑥⦌𝐵)
7	2, 6	eqtri 2788	. 2 ⊢ 𝐹 = (𝑦 ∈ 𝐶 ↦ ⦋𝑦 / 𝑥⦌𝐵)
8	1, 7	fvmptg 6991	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → (𝐹‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ⦋csb 3854   ↦ cmpt 5194  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548

This theorem is used by:  fvmptdf  7000  fvmpocurryd  8269  mptnn0fsupp  14046  mptnn0fsuppr  14048  zsum  15787  prodss  16019  fprodser  16021  fprodn0  16051  fprodefsum  16166  pcmpt  16969  issubc  17909  gsummptnn0fz  20079  mptscmfsupp0  21077  gsummoncoe1  22497  fvmptnn04if  23035  prdsdsf  24553  itgparts  26235  dchrisumlema  27681  abfmpeld  33028  abfmpel  33029  cdlemk40  41724  deg1gprod  42940  aomclem6  43819  ellimcabssub0  46366  constlimc  46373  vonn0ioo2  47437  vonn0icc2  47439  dftermo4  50313