Theorem offveq

Description: Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	offveq.1	$$⊢\phi \to A\in V$$
	offveq.2	$$⊢\phi \to FFnA$$
	offveq.3	$$⊢\phi \to GFnA$$
	offveq.4	$$⊢\phi \to HFnA$$
	offveq.5	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
	offveq.6	$$⊢\left(\phi \wedge x\in A\right)\to G\left(x\right)=C$$
	offveq.7	$$⊢\left(\phi \wedge x\in A\right)\to BRC=H\left(x\right)$$
Assertion	offveq	$$⊢\phi \to F{R}_{f}G=H$$

Proof

Step	Hyp	Ref	Expression
1		offveq.1	$$⊢\phi \to A\in V$$
2		offveq.2	$$⊢\phi \to FFnA$$
3		offveq.3	$$⊢\phi \to GFnA$$
4		offveq.4	$$⊢\phi \to HFnA$$
5		offveq.5	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
6		offveq.6	$$⊢\left(\phi \wedge x\in A\right)\to G\left(x\right)=C$$
7		offveq.7	$$⊢\left(\phi \wedge x\in A\right)\to BRC=H\left(x\right)$$
8		inidm	$$⊢A\cap A=A$$
9	2 3 1 1 8	offn	$$⊢\phi \to \left(F{R}_{f}G\right)FnA$$
10	2 3 1 1 8 5 6	ofval	$$⊢\left(\phi \wedge x\in A\right)\to \left(F{R}_{f}G\right)\left(x\right)=BRC$$
11	10 7	eqtrd	$$⊢\left(\phi \wedge x\in A\right)\to \left(F{R}_{f}G\right)\left(x\right)=H\left(x\right)$$
12	9 4 11	eqfnfvd	$$⊢\phi \to F{R}_{f}G=H$$