Metamath Proof Explorer


Theorem op2ndb

Description: Extract the second member of an ordered pair. Theorem 5.12(ii) of Monk1 p. 52. (See op1stb to extract the first member, op2nda for an alternate version, and op2nd for the preferred version.) (Contributed by NM, 25-Nov-2003)

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

Proof

Step Hyp Ref Expression
1 cnvsn.1 𝐴 ∈ V
2 cnvsn.2 𝐵 ∈ V
3 1 2 cnvsn { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ }
4 3 inteqi { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ }
5 opex 𝐵 , 𝐴 ⟩ ∈ V
6 5 intsn { ⟨ 𝐵 , 𝐴 ⟩ } = ⟨ 𝐵 , 𝐴
7 4 6 eqtri { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴
8 7 inteqi { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵 , 𝐴
9 8 inteqi { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵 , 𝐴
10 2 1 op1stb 𝐵 , 𝐴 ⟩ = 𝐵
11 9 10 eqtri { ⟨ 𝐴 , 𝐵 ⟩ } = 𝐵