Description: Extract the first member of an ordered triple. Deduction version. (Contributed by Scott Fenton, 21-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ot21st.1 | ⊢ 𝐴 ∈ V | |
ot21st.2 | ⊢ 𝐵 ∈ V | ||
ot21st.3 | ⊢ 𝐶 ∈ V | ||
Assertion | ot21std | ⊢ ( 𝑋 = 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 → ( 1st ‘ ( 1st ‘ 𝑋 ) ) = 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ot21st.1 | ⊢ 𝐴 ∈ V | |
2 | ot21st.2 | ⊢ 𝐵 ∈ V | |
3 | ot21st.3 | ⊢ 𝐶 ∈ V | |
4 | opex | ⊢ 〈 𝐴 , 𝐵 〉 ∈ V | |
5 | 4 3 | op1std | ⊢ ( 𝑋 = 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 → ( 1st ‘ 𝑋 ) = 〈 𝐴 , 𝐵 〉 ) |
6 | 5 | fveq2d | ⊢ ( 𝑋 = 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 → ( 1st ‘ ( 1st ‘ 𝑋 ) ) = ( 1st ‘ 〈 𝐴 , 𝐵 〉 ) ) |
7 | 1 2 | op1st | ⊢ ( 1st ‘ 〈 𝐴 , 𝐵 〉 ) = 𝐴 |
8 | 6 7 | eqtrdi | ⊢ ( 𝑋 = 〈 〈 𝐴 , 𝐵 〉 , 𝐶 〉 → ( 1st ‘ ( 1st ‘ 𝑋 ) ) = 𝐴 ) |