Metamath Proof Explorer

Theorem tpex

Description: An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994)

Ref Expression
Assertion tpex 
|- { A , B , C } e. _V

Proof

Step Hyp Ref Expression
1 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
2 prex 
 |-  { A , B } e. _V
3 snex 
 |-  { C } e. _V
4 2 3 unex 
 |-  ( { A , B } u. { C } ) e. _V
5 1 4 eqeltri 
 |-  { A , B , C } e. _V