Metamath Proof Explorer


Theorem op2nda

Description: Extract the second member of an ordered pair. (See op1sta to extract the first member, op2ndb for an alternate version, and op2nd for the preferred version.) (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Hypotheses cnvsn.1 𝐴 ∈ V
cnvsn.2 𝐵 ∈ V
Assertion op2nda ran { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵

Proof

Step Hyp Ref Expression
1 cnvsn.1 𝐴 ∈ V
2 cnvsn.2 𝐵 ∈ V
3 1 rnsnop ran { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐵 }
4 3 unieqi ran { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐵 }
5 2 unisn { 𝐵 } = 𝐵
6 4 5 eqtri ran { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵