Proof of Theorem fvmptd
Step | Hyp | Ref
| Expression |
1 | | fvmptd.1 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) |
2 | 1 | fveq1d 6193 |
. 2
⊢ (𝜑 → (𝐹‘𝐴) = ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴)) |
3 | | fvmptd.3 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐷) |
4 | | fvmptd.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) |
5 | 3, 4 | csbied 3560 |
. . . 4
⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
6 | | fvmptd.4 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
7 | 5, 6 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) |
8 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = (𝑥 ∈ 𝐷 ↦ 𝐵) |
9 | 8 | fvmpts 6285 |
. . 3
⊢ ((𝐴 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵) |
10 | 3, 7, 9 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐵)‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵) |
11 | 2, 10, 5 | 3eqtrd 2660 |
1
⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) |