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 | ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ ( ( 𝑅 × 𝑆 ) × 𝑇 ) → 𝐴 ∈ 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxp1 | ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ ( ( 𝑅 × 𝑆 ) × 𝑇 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) ) | |
2 | opelxp1 | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) → 𝐴 ∈ 𝑅 ) | |
3 | 1 2 | syl | ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ ( ( 𝑅 × 𝑆 ) × 𝑇 ) → 𝐴 ∈ 𝑅 ) |