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 3524 | . 2 |
5 | 1, 2 | cpr 3523 | . . 3 |
6 | 3 | csn 3522 | . . 3 |
7 | 5, 6 | cun 3064 | . 2 |
8 | 4, 7 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: eltpg 3564 raltpg 3571 rextpg 3572 tpeq1 3604 tpeq2 3605 tpeq3 3606 tpcoma 3612 tpass 3614 qdass 3615 tpidm12 3617 diftpsn3 3656 snsstp1 3665 snsstp2 3666 snsstp3 3667 prsstp12 3668 tpss 3680 tpssi 3681 ord3ex 4109 tpexg 4360 dmtpop 5009 funtpg 5169 funtp 5171 fntpg 5174 ftpg 5597 fvtp1g 5621 tpfidisj 6809 fztp 9851 sumtp 11176 strle3g 12040 bdctp 13059 |
Copyright terms: Public domain | W3C validator |