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