This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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