Theorem ot3rdg

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

	Ref	Expression
Assertion	ot3rdg	|- ( C e. V -> ( 2nd ` <. A , B , C >. ) = C )

Proof

Step	Hyp	Ref	Expression
1		df-ot	|- <. A , B , C >. = <. <. A , B >. , C >.
2	1	fveq2i	|- ( 2nd ` <. A , B , C >. ) = ( 2nd ` <. <. A , B >. , C >. )
3		opex	|- <. A , B >. e. _V
4		op2ndg	|- ( ( <. A , B >. e. _V /\ C e. V ) -> ( 2nd ` <. <. A , B >. , C >. ) = C )
5	3 4	mpan	|- ( C e. V -> ( 2nd ` <. <. A , B >. , C >. ) = C )
6	2 5	syl5eq	|- ( C e. V -> ( 2nd ` <. A , B , C >. ) = C )