Description: Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | csbfv2g | ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbfv12 | ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) | |
2 | csbconstg | ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = 𝐹 ) | |
3 | 2 | fveq1d | ⊢ ( 𝐴 ∈ 𝐶 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
4 | 1 3 | eqtrid | ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |