Theorem ot22ndd

Description: Extract the second member of an ordered triple. Deduction version. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Hypotheses	ot21st.1	$$⊢A\in \mathrm{V}$$
	ot21st.2	$$⊢B\in \mathrm{V}$$
	ot21st.3	$$⊢C\in \mathrm{V}$$
Assertion	ot22ndd	$$⊢X=⟨⟨A,B⟩,C⟩\to 2^{nd}\left(1^{st}\left(X\right)\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		ot21st.1	$$⊢A\in \mathrm{V}$$
2		ot21st.2	$$⊢B\in \mathrm{V}$$
3		ot21st.3	$$⊢C\in \mathrm{V}$$
4		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
5	4 3	op1std	$$⊢X=⟨⟨A,B⟩,C⟩\to 1^{st}\left(X\right)=⟨A,B⟩$$
6	5	fveq2d	$$⊢X=⟨⟨A,B⟩,C⟩\to 2^{nd}\left(1^{st}\left(X\right)\right)=2^{nd}\left(⟨A,B⟩\right)$$
7	1 2	op2nd	$$⊢2^{nd}\left(⟨A,B⟩\right)=B$$
8	6 7	eqtrdi	$$⊢X=⟨⟨A,B⟩,C⟩\to 2^{nd}\left(1^{st}\left(X\right)\right)=B$$