Theorem ofrfval

Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	offval.1	$$⊢\phi \to FFnA$$
	offval.2	$$⊢\phi \to GFnB$$
	offval.3	$$⊢\phi \to A\in V$$
	offval.4	$$⊢\phi \to B\in W$$
	offval.5	$$⊢A\cap B=S$$
	offval.6	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=C$$
	offval.7	$$⊢\left(\phi \wedge x\in B\right)\to G\left(x\right)=D$$
Assertion	ofrfval	$$⊢\phi \to \left(F{R}_{f}G\leftrightarrow \forall x\in SCRD\right)$$

Proof

Step	Hyp	Ref	Expression
1		offval.1	$$⊢\phi \to FFnA$$
2		offval.2	$$⊢\phi \to GFnB$$
3		offval.3	$$⊢\phi \to A\in V$$
4		offval.4	$$⊢\phi \to B\in W$$
5		offval.5	$$⊢A\cap B=S$$
6		offval.6	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=C$$
7		offval.7	$$⊢\left(\phi \wedge x\in B\right)\to G\left(x\right)=D$$
8	1 3	fnexd	$$⊢\phi \to F\in \mathrm{V}$$
9	2 4	fnexd	$$⊢\phi \to G\in \mathrm{V}$$
10	1 2 8 9 5 6 7	ofrfvalg	$$⊢\phi \to \left(F{R}_{f}G\leftrightarrow \forall x\in SCRD\right)$$