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⟩\in \left(\left(R\times S\right)\times T\right)\to A\in R$$

Proof

Step	Hyp	Ref	Expression
1		opelxp1	$$⊢⟨⟨A,B⟩,C⟩\in \left(\left(R\times S\right)\times T\right)\to ⟨A,B⟩\in \left(R\times S\right)$$
2		opelxp1	$$⊢⟨A,B⟩\in \left(R\times S\right)\to A\in R$$
3	1 2	syl	$$⊢⟨⟨A,B⟩,C⟩\in \left(\left(R\times S\right)\times T\right)\to A\in R$$