This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrdi ⊢ C = A B → 2 nd ⁡ C = B