Theorem fvmpts

Description: Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	fvmpts.1	$$⊢F=\left(x\in C⟼B\right)$$
Assertion	fvmpts	$$⊢\left(A\in C\wedge ⦋A/x⦌B\in V\right)\to F\left(A\right)=⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		fvmpts.1	$$⊢F=\left(x\in C⟼B\right)$$
2		csbeq1	$$⊢y=A\to ⦋y/x⦌B=⦋A/x⦌B$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
4		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
5		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
6	3 4 5	cbvmpt	$$⊢\left(x\in C⟼B\right)=\left(y\in C⟼⦋y/x⦌B\right)$$
7	1 6	eqtri	$$⊢F=\left(y\in C⟼⦋y/x⦌B\right)$$
8	2 7	fvmptg	$$⊢\left(A\in C\wedge ⦋A/x⦌B\in V\right)\to F\left(A\right)=⦋A/x⦌B$$