Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-tp | Structured version Visualization version Unicode 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 | |
2 | cB | . . 3 | |
3 | cC | . . 3 | |
4 | 1, 2, 3 | ctp 4181 | . 2 |
5 | 1, 2 | cpr 4179 | . . 3 |
6 | 3 | csn 4177 | . . 3 |
7 | 5, 6 | cun 3572 | . 2 |
8 | 4, 7 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: eltpg 4227 raltpg 4236 rextpg 4237 disjtpsn 4251 disjtp2 4252 tpeq1 4277 tpeq2 4278 tpeq3 4279 tpcoma 4285 tpass 4287 qdass 4288 tpidm12 4290 diftpsn3 4332 diftpsn3OLD 4333 tpprceq3 4335 tppreqb 4336 snsstp1 4347 snsstp2 4348 snsstp3 4349 sstp 4367 tpss 4368 tpssi 4369 ord3ex 4856 dmtpop 5611 funtpg 5942 funtpgOLD 5943 funtp 5945 fntpg 5948 funcnvtp 5951 ftpg 6423 fvtp1 6460 fvtp1g 6463 tpex 6957 fr3nr 6979 tpfi 8236 fztp 12397 hashtplei 13266 hashtpg 13267 s3tpop 13654 sumtp 14478 bpoly3 14789 strlemor3OLD 15971 strle3 15975 estrreslem2 16778 estrres 16779 lsptpcl 18979 perfectlem2 24955 ex-un 27281 ex-ss 27284 ex-pw 27286 ex-hash 27310 prodtp 29573 sltsolem1 31826 dvh4dimlem 36732 dvhdimlem 36733 dvh4dimN 36736 df3o2 38322 df3o3 38323 perfectALTVlem2 41631 |
Copyright terms: Public domain | W3C validator |