Theorem csbfv2g

Description: Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	csbfv2g	⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		csbfv12	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
2		csbconstg	⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = 𝐹 )
3	2	fveq1d	⊢ ( 𝐴 ∈ 𝐶 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
4	1 3	syl5eq	⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )