Theorem otex

Description: An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015)

	Ref	Expression
Assertion	otex	|- <. A , B , C >. e. _V

Proof

Step	Hyp	Ref	Expression
1		df-ot	|- <. A , B , C >. = <. <. A , B >. , C >.
2		opex	|- <. <. A , B >. , C >. e. _V
3	1 2	eqeltri	|- <. A , B , C >. e. _V