Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-tp | 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 3499 | . 2 |
5 | 1, 2 | cpr 3498 | . . 3 |
6 | 3 | csn 3497 | . . 3 |
7 | 5, 6 | cun 3039 | . 2 |
8 | 4, 7 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: eltpg 3539 raltpg 3546 rextpg 3547 tpeq1 3579 tpeq2 3580 tpeq3 3581 tpcoma 3587 tpass 3589 qdass 3590 tpidm12 3592 diftpsn3 3631 snsstp1 3640 snsstp2 3641 snsstp3 3642 prsstp12 3643 tpss 3655 tpssi 3656 ord3ex 4084 tpexg 4335 dmtpop 4984 funtpg 5144 funtp 5146 fntpg 5149 ftpg 5572 fvtp1g 5596 tpfidisj 6784 fztp 9813 sumtp 11138 strle3g 11962 bdctp 12966 |
Copyright terms: Public domain | W3C validator |