Metamath Proof Explorer


Theorem otex

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

Ref Expression
Assertion otex A B C V

Proof

Step Hyp Ref Expression
1 df-ot A B C = A B C
2 opex A B C V
3 1 2 eqeltri A B C V