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 4563 | . 2 class {𝐴, 𝐵, 𝐶} |
5 | 1, 2 | cpr 4561 | . . 3 class {𝐴, 𝐵} |
6 | 3 | csn 4559 | . . 3 class {𝐶} |
7 | 5, 6 | cun 3933 | . 2 class ({𝐴, 𝐵} ∪ {𝐶}) |
8 | 4, 7 | wceq 1528 | 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
Colors of variables: wff setvar class |
This definition is referenced by: eltpg 4617 raltpg 4628 rextpg 4629 disjtpsn 4645 disjtp2 4646 tpeq1 4672 tpeq2 4673 tpeq3 4674 tpcoma 4680 tpass 4682 qdass 4683 tpidm12 4685 diftpsn3 4729 tpprceq3 4731 tppreqb 4732 snsstp1 4743 snsstp2 4744 snsstp3 4745 sstp 4761 tpss 4762 tpssi 4763 ord3ex 5279 dmtpop 6069 funtpg 6403 funtp 6405 fntpg 6408 funcnvtp 6411 ftpg 6911 fvtp1 6950 fvtp1g 6953 tpex 7458 fr3nr 7482 tpfi 8783 fztp 12953 hashtplei 13832 hashtpg 13833 s3tpop 14261 sumtp 15094 bpoly3 15402 strle3 16584 estrreslem2 17378 estrres 17379 lsptpcl 19682 perfectlem2 25734 ex-un 28131 ex-ss 28134 ex-pw 28136 ex-hash 28160 fnimatp 30352 prodtp 30471 sltsolem1 33078 dvh4dimlem 38461 dvhdimlem 38462 dvh4dimN 38465 tr3dom 39774 df3o2 40254 df3o3 40255 perfectALTVlem2 43734 |
Copyright terms: Public domain | W3C validator |