Theorem op2nd

Description: Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004)

	Ref	Expression
Hypotheses	op1st.1	⊢ 𝐴 ∈ V
	op1st.2	⊢ 𝐵 ∈ V
Assertion	op2nd	⊢ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵

Proof

Step	Hyp	Ref	Expression
1		op1st.1	⊢ 𝐴 ∈ V
2		op1st.2	⊢ 𝐵 ∈ V
3		2ndval	⊢ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∪ ran { ⟨ 𝐴 , 𝐵 ⟩ }
4	1 2	op2nda	⊢ ∪ ran { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵
5	3 4	eqtri	⊢ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵