Theorem csbfv

Description: Substitution for a function value. (Contributed by NM, 1-Jan-2006) (Revised by NM, 20-Aug-2018)

	Ref	Expression
Assertion	csbfv	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		csbfv2g	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑥 ) )
2		csbvarg	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )
3	2	fveq2d	⊢ ( 𝐴 ∈ V → ( 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
4	1 3	eqtrd	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
5		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝑥 ) = ∅ )
6		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )
7	5 6	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
8	4 7	pm2.61i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 )