Theorem ofcval

Description: Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval.1	$$⊢\phi \to FFnA$$
	ofcfval.2	$$⊢\phi \to A\in V$$
	ofcfval.3	$$⊢\phi \to C\in W$$
	ofcval.6	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)=B$$
Assertion	ofcval	$$⊢\left(\phi \wedge X\in A\right)\to \left(F{\circ }_{\mathrm{fc}}RC\right)\left(X\right)=BRC$$

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	$$⊢\phi \to FFnA$$
2		ofcfval.2	$$⊢\phi \to A\in V$$
3		ofcfval.3	$$⊢\phi \to C\in W$$
4		ofcval.6	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)=B$$
5		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
6	1 2 3 5	ofcfval	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(x\in A⟼F\left(x\right)RC\right)$$
7	6	adantr	$$⊢\left(\phi \wedge X\in A\right)\to F{\circ }_{\mathrm{fc}}RC=\left(x\in A⟼F\left(x\right)RC\right)$$
8		simpr	$$⊢\left(\left(\phi \wedge X\in A\right)\wedge x=X\right)\to x=X$$
9	8	fveq2d	$$⊢\left(\left(\phi \wedge X\in A\right)\wedge x=X\right)\to F\left(x\right)=F\left(X\right)$$
10	9	oveq1d	$$⊢\left(\left(\phi \wedge X\in A\right)\wedge x=X\right)\to F\left(x\right)RC=F\left(X\right)RC$$
11		simpr	$$⊢\left(\phi \wedge X\in A\right)\to X\in A$$
12		ovexd	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)RC\in \mathrm{V}$$
13	7 10 11 12	fvmptd	$$⊢\left(\phi \wedge X\in A\right)\to \left(F{\circ }_{\mathrm{fc}}RC\right)\left(X\right)=F\left(X\right)RC$$
14	4	oveq1d	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)RC=BRC$$
15	13 14	eqtrd	$$⊢\left(\phi \wedge X\in A\right)\to \left(F{\circ }_{\mathrm{fc}}RC\right)\left(X\right)=BRC$$