Theorem ofc12

Description: Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	ofc12.1	|- ( ph -> A e. V )
	ofc12.2	|- ( ph -> B e. W )
	ofc12.3	|- ( ph -> C e. X )
Assertion	ofc12	|- ( ph -> ( ( A X. { B } ) oF R ( A X. { C } ) ) = ( A X. { ( B R C ) } ) )

Proof

Step	Hyp	Ref	Expression
1		ofc12.1	|- ( ph -> A e. V )
2		ofc12.2	|- ( ph -> B e. W )
3		ofc12.3	|- ( ph -> C e. X )
4	2	adantr	|- ( ( ph /\ x e. A ) -> B e. W )
5	3	adantr	|- ( ( ph /\ x e. A ) -> C e. X )
6		fconstmpt	|- ( A X. { B } ) = ( x e. A |-> B )
7	6	a1i	|- ( ph -> ( A X. { B } ) = ( x e. A |-> B ) )
8		fconstmpt	|- ( A X. { C } ) = ( x e. A |-> C )
9	8	a1i	|- ( ph -> ( A X. { C } ) = ( x e. A |-> C ) )
10	1 4 5 7 9	offval2	|- ( ph -> ( ( A X. { B } ) oF R ( A X. { C } ) ) = ( x e. A |-> ( B R C ) ) )
11		fconstmpt	|- ( A X. { ( B R C ) } ) = ( x e. A |-> ( B R C ) )
12	10 11	eqtr4di	|- ( ph -> ( ( A X. { B } ) oF R ( A X. { C } ) ) = ( A X. { ( B R C ) } ) )