![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-tp | Structured version Visualization version GIF version |
Description: Define unordered triple
of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4639. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
Ref | Expression |
---|---|
df-tp | ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cC | . . 3 class 𝐶 | |
4 | 1, 2, 3 | ctp 4634 | . 2 class {𝐴, 𝐵, 𝐶} |
5 | 1, 2 | cpr 4632 | . . 3 class {𝐴, 𝐵} |
6 | 3 | csn 4630 | . . 3 class {𝐶} |
7 | 5, 6 | cun 3942 | . 2 class ({𝐴, 𝐵} ∪ {𝐶}) |
8 | 4, 7 | wceq 1533 | 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
Colors of variables: wff setvar class |
This definition is referenced by: eltpg 4691 raltpg 4704 rextpg 4705 disjtpsn 4721 disjtp2 4722 tpeq1 4748 tpeq2 4749 tpeq3 4750 tpcoma 4756 tpass 4758 qdass 4759 tpidm12 4761 diftpsn3 4807 tpprceq3 4809 tppreqb 4810 snsstp1 4821 snsstp2 4822 snsstp3 4823 sstp 4839 tpss 4840 tpssi 4841 ord3ex 5387 dmtpop 6224 funtpg 6609 funtp 6611 fntpg 6614 funcnvtp 6617 ftpg 7165 fvtp1 7207 fvtp1g 7210 tpex 7750 fr3nr 7775 tpfi 9349 fztp 13592 hashtplei 14481 hashtpg 14482 s3tpop 14896 sumtp 15731 bpoly3 16038 strle3 17132 estrreslem2 18132 estrres 18133 lsptpcl 20875 perfectlem2 27208 sltsolem1 27654 ex-un 30306 ex-ss 30309 ex-pw 30311 ex-hash 30335 fnimatp 32544 prodtp 32675 dvh4dimlem 41046 dvhdimlem 41047 dvh4dimN 41050 df3o2 42884 df3o3 42885 omcl3g 42905 onsucunitp 42944 oaun3 42953 tr3dom 43100 perfectALTVlem2 47199 |
Copyright terms: Public domain | W3C validator |