Theorem offvalfv

Description: The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019)

	Ref	Expression
Hypotheses	offvalfv.a	$$⊢\phi \to A\in V$$
	offvalfv.f	$$⊢\phi \to FFnA$$
	offvalfv.g	$$⊢\phi \to GFnA$$
Assertion	offvalfv	$$⊢\phi \to F{R}_{f}G=\left(x\in A⟼F\left(x\right)RG\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		offvalfv.a	$$⊢\phi \to A\in V$$
2		offvalfv.f	$$⊢\phi \to FFnA$$
3		offvalfv.g	$$⊢\phi \to GFnA$$
4		fnfvelrn	$$⊢\left(FFnA\wedge x\in A\right)\to F\left(x\right)\in \mathrm{ran}F$$
5	2 4	sylan	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in \mathrm{ran}F$$
6		fnfvelrn	$$⊢\left(GFnA\wedge x\in A\right)\to G\left(x\right)\in \mathrm{ran}G$$
7	3 6	sylan	$$⊢\left(\phi \wedge x\in A\right)\to G\left(x\right)\in \mathrm{ran}G$$
8		dffn5	$$⊢FFnA\leftrightarrow F=\left(x\in A⟼F\left(x\right)\right)$$
9	2 8	sylib	$$⊢\phi \to F=\left(x\in A⟼F\left(x\right)\right)$$
10		dffn5	$$⊢GFnA\leftrightarrow G=\left(x\in A⟼G\left(x\right)\right)$$
11	3 10	sylib	$$⊢\phi \to G=\left(x\in A⟼G\left(x\right)\right)$$
12	1 5 7 9 11	offval2	$$⊢\phi \to F{R}_{f}G=\left(x\in A⟼F\left(x\right)RG\left(x\right)\right)$$