Theorem op2ndd

Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		op1st.1	$$⊢A\in \mathrm{V}$$
2		op1st.2	$$⊢B\in \mathrm{V}$$
3		fveq2	$$⊢C=⟨A,B⟩\to 2^{nd}\left(C\right)=2^{nd}\left(⟨A,B⟩\right)$$
4	1 2	op2nd	$$⊢2^{nd}\left(⟨A,B⟩\right)=B$$
5	3 4	eqtrdi	$$⊢C=⟨A,B⟩\to 2^{nd}\left(C\right)=B$$