Metamath Proof Explorer


Theorem ot21std

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𝑋 ) ) = 𝐴 )

Proof

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𝑋 ) ) = 𝐴 )