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
|- A e. _V
ot21st.2
|- B e. _V
ot21st.3
|- C e. _V
Assertion ot21std
|- ( X = <. <. A , B >. , C >. -> ( 1st ` ( 1st ` X ) ) = A )

Proof

Step Hyp Ref Expression
1 ot21st.1
 |-  A e. _V
2 ot21st.2
 |-  B e. _V
3 ot21st.3
 |-  C e. _V
4 opex
 |-  <. A , B >. e. _V
5 4 3 op1std
 |-  ( X = <. <. A , B >. , C >. -> ( 1st ` X ) = <. A , B >. )
6 5 fveq2d
 |-  ( X = <. <. A , B >. , C >. -> ( 1st ` ( 1st ` X ) ) = ( 1st ` <. A , B >. ) )
7 1 2 op1st
 |-  ( 1st ` <. A , B >. ) = A
8 6 7 eqtrdi
 |-  ( X = <. <. A , B >. , C >. -> ( 1st ` ( 1st ` X ) ) = A )