| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fvmpts | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| fvmpts.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐶 ↦ 𝐵) |
| Ref | Expression |
|---|---|
| fvmpts | ⊢ ((𝐴 ∈ 𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → (𝐹‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | csbeq1 3850 | . 2 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵) | |
| 2 | fvmpts.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶 ↦ 𝐵) | |
| 3 | nfcv 2896 | . . . 4 ⊢ Ⅎ𝑦𝐵 | |
| 4 | nfcsb1v 3871 | . . . 4 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 | |
| 5 | csbeq1a 3861 | . . . 4 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) | |
| 6 | 3, 4, 5 | cbvmpt 5197 | . . 3 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
| 7 | 2, 6 | eqtri 2756 | . 2 ⊢ 𝐹 = (𝑦 ∈ 𝐶 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
| 8 | 1, 7 | fvmptg 6936 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → (𝐹‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ⦋csb 3847 ↦ cmpt 5176 ‘cfv 6489 |
| 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 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pr 5374 |
| 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 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2883 df-ral 3050 df-rex 3059 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-ss 3916 df-nul 4285 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5516 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-iota 6445 df-fun 6491 df-fv 6497 |
| This theorem is referenced by: fvmptdf 6944 fvmpocurryd 8210 mptnn0fsupp 13914 mptnn0fsuppr 13916 zsum 15635 prodss 15864 fprodser 15866 fprodn0 15896 fprodefsum 16012 pcmpt 16814 issubc 17752 gsummptnn0fz 19908 mptscmfsupp0 20870 gsummoncoe1 22233 fvmptnn04if 22774 prdsdsf 24292 itgparts 25991 dchrisumlema 27436 abfmpeld 32647 abfmpel 32648 cdlemk40 41026 deg1gprod 42243 aomclem6 43166 ellimcabssub0 45731 constlimc 45738 vonn0ioo2 46802 vonn0icc2 46804 dftermo4 49617 |
| Copyright terms: Public domain | W3C validator |