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	syl5eq	⊢ ( 𝐶 ∈ 𝑉 → ( 2nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 )