Theorem ovconst2

Description: The value of a constant operation. (Contributed by NM, 5-Nov-2006)

	Ref	Expression
Hypothesis	oprvalconst2.1	|- C e. _V
Assertion	ovconst2	|- ( ( R e. A /\ S e. B ) -> ( R ( ( A X. B ) X. { C } ) S ) = C )

Proof

Step	Hyp	Ref	Expression
1		oprvalconst2.1	|- C e. _V
2		df-ov	|- ( R ( ( A X. B ) X. { C } ) S ) = ( ( ( A X. B ) X. { C } ) ` <. R , S >. )
3		opelxpi	|- ( ( R e. A /\ S e. B ) -> <. R , S >. e. ( A X. B ) )
4	1	fvconst2	|- ( <. R , S >. e. ( A X. B ) -> ( ( ( A X. B ) X. { C } ) ` <. R , S >. ) = C )
5	3 4	syl	|- ( ( R e. A /\ S e. B ) -> ( ( ( A X. B ) X. { C } ) ` <. R , S >. ) = C )
6	2 5	syl5eq	|- ( ( R e. A /\ S e. B ) -> ( R ( ( A X. B ) X. { C } ) S ) = C )