Theorem ofrfval

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

	Ref	Expression
Hypotheses	offval.1	|- ( ph -> F Fn A )
	offval.2	|- ( ph -> G Fn B )
	offval.3	|- ( ph -> A e. V )
	offval.4	|- ( ph -> B e. W )
	offval.5	|- ( A i^i B ) = S
	offval.6	|- ( ( ph /\ x e. A ) -> ( F ` x ) = C )
	offval.7	|- ( ( ph /\ x e. B ) -> ( G ` x ) = D )
Assertion	ofrfval	|- ( ph -> ( F oR R G <-> A. x e. S C R D ) )

Proof

Step	Hyp	Ref	Expression
1		offval.1	|- ( ph -> F Fn A )
2		offval.2	|- ( ph -> G Fn B )
3		offval.3	|- ( ph -> A e. V )
4		offval.4	|- ( ph -> B e. W )
5		offval.5	|- ( A i^i B ) = S
6		offval.6	|- ( ( ph /\ x e. A ) -> ( F ` x ) = C )
7		offval.7	|- ( ( ph /\ x e. B ) -> ( G ` x ) = D )
8	1 3	fnexd	|- ( ph -> F e. _V )
9	2 4	fnexd	|- ( ph -> G e. _V )
10	1 2 8 9 5 6 7	ofrfvalg	|- ( ph -> ( F oR R G <-> A. x e. S C R D ) )