Theorem otelxp1

Description: The first member of an ordered triple of classes in a Cartesian product belongs to first Cartesian product argument. (Contributed by NM, 28-May-2008)

	Ref	Expression
Assertion	otelxp1	|- ( <. <. A , B >. , C >. e. ( ( R X. S ) X. T ) -> A e. R )

Proof

Step	Hyp	Ref	Expression
1		opelxp1	|- ( <. <. A , B >. , C >. e. ( ( R X. S ) X. T ) -> <. A , B >. e. ( R X. S ) )
2		opelxp1	|- ( <. A , B >. e. ( R X. S ) -> A e. R )
3	1 2	syl	|- ( <. <. A , B >. , C >. e. ( ( R X. S ) X. T ) -> A e. R )