![]() |
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. (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 4323 | . 2 class {𝐴, 𝐵, 𝐶} |
5 | 1, 2 | cpr 4321 | . . 3 class {𝐴, 𝐵} |
6 | 3 | csn 4319 | . . 3 class {𝐶} |
7 | 5, 6 | cun 3711 | . 2 class ({𝐴, 𝐵} ∪ {𝐶}) |
8 | 4, 7 | wceq 1630 | 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
Colors of variables: wff setvar class |
This definition is referenced by: eltpg 4369 raltpg 4378 rextpg 4379 disjtpsn 4393 disjtp2 4394 tpeq1 4419 tpeq2 4420 tpeq3 4421 tpcoma 4427 tpass 4429 qdass 4430 tpidm12 4432 diftpsn3 4475 diftpsn3OLD 4476 tpprceq3 4478 tppreqb 4479 snsstp1 4490 snsstp2 4491 snsstp3 4492 sstp 4510 tpss 4511 tpssi 4512 ord3ex 5003 dmtpop 5768 funtpg 6101 funtpgOLD 6102 funtp 6104 fntpg 6107 funcnvtp 6110 ftpg 6584 fvtp1 6622 fvtp1g 6625 tpex 7120 fr3nr 7142 tpfi 8399 fztp 12588 hashtplei 13456 hashtpg 13457 s3tpop 13852 sumtp 14675 bpoly3 14986 strlemor3OLD 16171 strle3 16175 estrreslem2 16977 estrres 16978 lsptpcl 19179 perfectlem2 25152 ex-un 27590 ex-ss 27593 ex-pw 27595 ex-hash 27619 prodtp 29880 sltsolem1 32130 dvh4dimlem 37232 dvhdimlem 37233 dvh4dimN 37236 df3o2 38822 df3o3 38823 perfectALTVlem2 42139 |
Copyright terms: Public domain | W3C validator |