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 ) |
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 ) |