Theorem otex

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

	Ref	Expression
Assertion	otex	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-ot	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩
2		opex	⊢ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ V
3	1 2	eqeltri	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ V