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 4129 | . 2 class {𝐴, 𝐵, 𝐶} |
5 | 1, 2 | cpr 4127 | . . 3 class {𝐴, 𝐵} |
6 | 3 | csn 4125 | . . 3 class {𝐶} |
7 | 5, 6 | cun 3538 | . 2 class ({𝐴, 𝐵} ∪ {𝐶}) |
8 | 4, 7 | wceq 1475 | 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
Colors of variables: wff setvar class |
This definition is referenced by: eltpg 4174 raltpg 4183 rextpg 4184 tpeq1 4221 tpeq2 4222 tpeq3 4223 tpcoma 4229 tpass 4231 qdass 4232 tpidm12 4234 diftpsn3 4273 diftpsn3OLD 4274 tpprceq3 4276 tppreqb 4277 snsstp1 4287 snsstp2 4288 snsstp3 4289 sstp 4307 tpss 4308 tpssi 4309 ord3ex 4782 dmtpop 5529 funtpg 5856 funtpgOLD 5857 funtp 5859 fntpg 5862 funcnvtp 5865 ftpg 6328 fvtp1 6365 fvtp1g 6368 tpex 6855 fr3nr 6871 tpfi 8121 fztp 12267 hashtplei 13120 hashtpg 13121 s3tpop 13504 sumtp 14322 bpoly3 14628 strlemor3 15798 strle3 15802 estrreslem2 16601 estrres 16602 lsptpcl 18800 perfectlem2 24755 constr2spthlem1 26124 ex-un 26673 ex-ss 26676 ex-pw 26678 ex-hash 26702 sltsolem1 31067 dvh4dimlem 35750 dvhdimlem 35751 dvh4dimN 35754 df3o2 37342 df3o3 37343 perfectALTVlem2 40165 |
Copyright terms: Public domain | W3C validator |