Theorem ofcfeqd2

Description: Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfeqd2.1	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
	ofcfeqd2.2	|- ( ( ph /\ y e. B ) -> ( y R C ) = ( y P C ) )
	ofcfeqd2.3	|- ( ph -> F Fn A )
	ofcfeqd2.4	|- ( ph -> A e. V )
	ofcfeqd2.5	|- ( ph -> C e. W )
Assertion	ofcfeqd2	|- ( ph -> ( F oFC R C ) = ( F oFC P C ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfeqd2.1	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
2		ofcfeqd2.2	|- ( ( ph /\ y e. B ) -> ( y R C ) = ( y P C ) )
3		ofcfeqd2.3	|- ( ph -> F Fn A )
4		ofcfeqd2.4	|- ( ph -> A e. V )
5		ofcfeqd2.5	|- ( ph -> C e. W )
6		oveq1	|- ( y = ( F ` x ) -> ( y R C ) = ( ( F ` x ) R C ) )
7		oveq1	|- ( y = ( F ` x ) -> ( y P C ) = ( ( F ` x ) P C ) )
8	6 7	eqeq12d	|- ( y = ( F ` x ) -> ( ( y R C ) = ( y P C ) <-> ( ( F ` x ) R C ) = ( ( F ` x ) P C ) ) )
9	2	ralrimiva	|- ( ph -> A. y e. B ( y R C ) = ( y P C ) )
10	9	adantr	|- ( ( ph /\ x e. A ) -> A. y e. B ( y R C ) = ( y P C ) )
11	8 10 1	rspcdva	|- ( ( ph /\ x e. A ) -> ( ( F ` x ) R C ) = ( ( F ` x ) P C ) )
12	11	mpteq2dva	|- ( ph -> ( x e. A |-> ( ( F ` x ) R C ) ) = ( x e. A |-> ( ( F ` x ) P C ) ) )
13		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
14	3 4 5 13	ofcfval	|- ( ph -> ( F oFC R C ) = ( x e. A |-> ( ( F ` x ) R C ) ) )
15	3 4 5 13	ofcfval	|- ( ph -> ( F oFC P C ) = ( x e. A |-> ( ( F ` x ) P C ) ) )
16	12 14 15	3eqtr4d	|- ( ph -> ( F oFC R C ) = ( F oFC P C ) )