Theorem ofcfeqd2

Description: Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfeqd2.1	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in B$$
	ofcfeqd2.2	$$⊢\left(\phi \wedge y\in B\right)\to yRC=yPC$$
	ofcfeqd2.3	$$⊢\phi \to FFnA$$
	ofcfeqd2.4	$$⊢\phi \to A\in V$$
	ofcfeqd2.5	$$⊢\phi \to C\in W$$
Assertion	ofcfeqd2	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=F{\circ }_{\mathrm{fc}}PC$$

Proof

Step	Hyp	Ref	Expression
1		ofcfeqd2.1	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in B$$
2		ofcfeqd2.2	$$⊢\left(\phi \wedge y\in B\right)\to yRC=yPC$$
3		ofcfeqd2.3	$$⊢\phi \to FFnA$$
4		ofcfeqd2.4	$$⊢\phi \to A\in V$$
5		ofcfeqd2.5	$$⊢\phi \to C\in W$$
6		oveq1	$$⊢y=F\left(x\right)\to yRC=F\left(x\right)RC$$
7		oveq1	$$⊢y=F\left(x\right)\to yPC=F\left(x\right)PC$$
8	6 7	eqeq12d	$$⊢y=F\left(x\right)\to \left(yRC=yPC\leftrightarrow F\left(x\right)RC=F\left(x\right)PC\right)$$
9	2	ralrimiva	$$⊢\phi \to \forall y\in ByRC=yPC$$
10	9	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \forall y\in ByRC=yPC$$
11	8 10 1	rspcdva	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)RC=F\left(x\right)PC$$
12	11	mpteq2dva	$$⊢\phi \to \left(x\in A⟼F\left(x\right)RC\right)=\left(x\in A⟼F\left(x\right)PC\right)$$
13		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
14	3 4 5 13	ofcfval	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=\left(x\in A⟼F\left(x\right)RC\right)$$
15	3 4 5 13	ofcfval	$$⊢\phi \to F{\circ }_{\mathrm{fc}}PC=\left(x\in A⟼F\left(x\right)PC\right)$$
16	12 14 15	3eqtr4d	$$⊢\phi \to F{\circ }_{\mathrm{fc}}RC=F{\circ }_{\mathrm{fc}}PC$$