Metamath Proof Explorer

Definition df-tp

Description: Define unordered triple of classes. Definition of Enderton p. 19.

Note: ordered triples are a completely different object defined below in df-ot . As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994)

Ref Expression
Assertion df-tp A B C = A B C

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cB class B
2 cC class C
3 0 1 2 ctp class A B C
4 0 1 cpr class A B
5 2 csn class C
6 4 5 cun class A B C
7 3 6 wceq wff A B C = A B C