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	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ ( ( 𝑅 × 𝑆 ) × 𝑇 ) → 𝐴 ∈ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		opelxp1	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ ( ( 𝑅 × 𝑆 ) × 𝑇 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) )
2		opelxp1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) → 𝐴 ∈ 𝑅 )
3	1 2	syl	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ ( ( 𝑅 × 𝑆 ) × 𝑇 ) → 𝐴 ∈ 𝑅 )