Description: Extract the third member of an ordered triple. (See ot1stg comment.) (Contributed by NM, 3-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ot3rdg | ⊢ ( 𝐶 ∈ 𝑉 → ( 2nd ‘ 〈 𝐴 , 𝐵 , 𝐶 〉 ) = 𝐶 ) |
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 ‘ 〈 𝐴 , 𝐵 , 𝐶 〉 ) = 𝐶 ) |