Theorem otth

Description: Ordered triple theorem. (Contributed by NM, 25-Sep-2014) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	otth.1	|- A e. _V
	otth.2	|- B e. _V
	otth.3	|- R e. _V
Assertion	otth	|- ( <. A , B , R >. = <. C , D , S >. <-> ( A = C /\ B = D /\ R = S ) )

Proof

Step	Hyp	Ref	Expression
1		otth.1	|- A e. _V
2		otth.2	|- B e. _V
3		otth.3	|- R e. _V
4		df-ot	|- <. A , B , R >. = <. <. A , B >. , R >.
5		df-ot	|- <. C , D , S >. = <. <. C , D >. , S >.
6	4 5	eqeq12i	|- ( <. A , B , R >. = <. C , D , S >. <-> <. <. A , B >. , R >. = <. <. C , D >. , S >. )
7	1 2 3	otth2	|- ( <. <. A , B >. , R >. = <. <. C , D >. , S >. <-> ( A = C /\ B = D /\ R = S ) )
8	6 7	bitri	|- ( <. A , B , R >. = <. C , D , S >. <-> ( A = C /\ B = D /\ R = S ) )