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 >. 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