Metamath Proof Explorer


Theorem op2ndd

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

Ref Expression
Hypotheses op1st.1 A V
op1st.2 B V
Assertion op2ndd C = A B 2 nd C = B

Proof

Step Hyp Ref Expression
1 op1st.1 A V
2 op1st.2 B V
3 fveq2 C = A B 2 nd C = 2 nd A B
4 1 2 op2nd 2 nd A B = B
5 3 4 syl6eq C = A B 2 nd C = B