![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-tp | 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 3609 | . 2 class {𝐴, 𝐵, 𝐶} |
5 | 1, 2 | cpr 3608 | . . 3 class {𝐴, 𝐵} |
6 | 3 | csn 3607 | . . 3 class {𝐶} |
7 | 5, 6 | cun 3142 | . 2 class ({𝐴, 𝐵} ∪ {𝐶}) |
8 | 4, 7 | wceq 1364 | 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
Colors of variables: wff set class |
This definition is referenced by: eltpg 3652 raltpg 3660 rextpg 3661 tpeq1 3693 tpeq2 3694 tpeq3 3695 tpcoma 3701 tpass 3703 qdass 3704 tpidm12 3706 diftpsn3 3748 snsstp1 3757 snsstp2 3758 snsstp3 3759 prsstp12 3760 tpss 3773 tpssi 3774 ord3ex 4208 tpexg 4462 dmtpop 5122 funtpg 5286 funtp 5288 fntpg 5291 ftpg 5721 fvtp1g 5745 tpfidisj 6957 fztp 10110 sumtp 11457 strle3g 12623 lsptpcl 13727 bdctp 15102 |
Copyright terms: Public domain | W3C validator |