Metamath Proof Explorer


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