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

Proof

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