Metamath Proof Explorer


Theorem ot3rdg

Description: Extract the third member of an ordered triple. (See ot1stg comment.) (Contributed by NM, 3-Apr-2015)

Ref Expression
Assertion ot3rdg ( 𝐶𝑉 → ( 2nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 df-ot 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶
2 1 fveq2i ( 2nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = ( 2nd ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ )
3 opex 𝐴 , 𝐵 ⟩ ∈ V
4 op2ndg ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ 𝐶𝑉 ) → ( 2nd ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) = 𝐶 )
5 3 4 mpan ( 𝐶𝑉 → ( 2nd ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) = 𝐶 )
6 2 5 eqtrid ( 𝐶𝑉 → ( 2nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 )