Theorem otex

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

	Ref	Expression
Assertion	otex	$$⊢⟨A,B,C⟩\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-ot	$$⊢⟨A,B,C⟩=⟨⟨A,B⟩,C⟩$$
2		opex	$$⊢⟨⟨A,B⟩,C⟩\in \mathrm{V}$$
3	1 2	eqeltri	$$⊢⟨A,B,C⟩\in \mathrm{V}$$