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 { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cB 𝐵
2 cC 𝐶
3 0 1 2 ctp { 𝐴 , 𝐵 , 𝐶 }
4 0 1 cpr { 𝐴 , 𝐵 }
5 2 csn { 𝐶 }
6 4 5 cun ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
7 3 6 wceq { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )