![]() |
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 3495 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | cpr 3494 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3 | csn 3493 |
. . 3
![]() ![]() ![]() ![]() |
7 | 5, 6 | cun 3035 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | wceq 1314 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: eltpg 3535 raltpg 3542 rextpg 3543 tpeq1 3575 tpeq2 3576 tpeq3 3577 tpcoma 3583 tpass 3585 qdass 3586 tpidm12 3588 diftpsn3 3627 snsstp1 3636 snsstp2 3637 snsstp3 3638 prsstp12 3639 tpss 3651 tpssi 3652 ord3ex 4074 tpexg 4325 dmtpop 4972 funtpg 5132 funtp 5134 fntpg 5137 ftpg 5558 fvtp1g 5582 tpfidisj 6769 fztp 9751 sumtp 11075 strle3g 11894 bdctp 12762 |
Copyright terms: Public domain | W3C validator |