Theorem csbfv

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

	Ref	Expression
Assertion	csbfv	$$⊢⦋A/x⦌F\left(x\right)=F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbfv2g	$$⊢A\in \mathrm{V}\to ⦋A/x⦌F\left(x\right)=F\left(⦋A/x⦌x\right)$$
2		csbvarg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌x=A$$
3	2	fveq2d	$$⊢A\in \mathrm{V}\to F\left(⦋A/x⦌x\right)=F\left(A\right)$$
4	1 3	eqtrd	$$⊢A\in \mathrm{V}\to ⦋A/x⦌F\left(x\right)=F\left(A\right)$$
5		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left(x\right)=\varnothing$$
6		fvprc	$$⊢\neg A\in \mathrm{V}\to F\left(A\right)=\varnothing$$
7	5 6	eqtr4d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left(x\right)=F\left(A\right)$$
8	4 7	pm2.61i	$$⊢⦋A/x⦌F\left(x\right)=F\left(A\right)$$