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	|- ( ph -> A e. V )
	offveq.2	|- ( ph -> F Fn A )
	offveq.3	|- ( ph -> G Fn A )
	offveq.4	|- ( ph -> H Fn A )
	offveq.5	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
	offveq.6	|- ( ( ph /\ x e. A ) -> ( G ` x ) = C )
	offveq.7	|- ( ( ph /\ x e. A ) -> ( B R C ) = ( H ` x ) )
Assertion	offveq	|- ( ph -> ( F oF R G ) = H )

Proof

Step	Hyp	Ref	Expression
1		offveq.1	|- ( ph -> A e. V )
2		offveq.2	|- ( ph -> F Fn A )
3		offveq.3	|- ( ph -> G Fn A )
4		offveq.4	|- ( ph -> H Fn A )
5		offveq.5	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
6		offveq.6	|- ( ( ph /\ x e. A ) -> ( G ` x ) = C )
7		offveq.7	|- ( ( ph /\ x e. A ) -> ( B R C ) = ( H ` x ) )
8		inidm	|- ( A i^i A ) = A
9	2 3 1 1 8	offn	|- ( ph -> ( F oF R G ) Fn A )
10	2 3 1 1 8 5 6	ofval	|- ( ( ph /\ x e. A ) -> ( ( F oF R G ) ` x ) = ( B R C ) )
11	10 7	eqtrd	|- ( ( ph /\ x e. A ) -> ( ( F oF R G ) ` x ) = ( H ` x ) )
12	9 4 11	eqfnfvd	|- ( ph -> ( F oF R G ) = H )