New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 | ⊢ {A, B, C} = ({A, B} ∪ {C}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | cC | . . 3 class C | |
4 | 1, 2, 3 | ctp 3739 | . 2 class {A, B, C} |
5 | 1, 2 | cpr 3738 | . . 3 class {A, B} |
6 | 3 | csn 3737 | . . 3 class {C} |
7 | 5, 6 | cun 3207 | . 2 class ({A, B} ∪ {C}) |
8 | 4, 7 | wceq 1642 | 1 wff {A, B, C} = ({A, B} ∪ {C}) |
Colors of variables: wff setvar class |
This definition is referenced by: eltpg 3769 raltpg 3777 rextpg 3778 tpeq1 3808 tpeq2 3809 tpeq3 3810 tpcoma 3816 tpass 3818 qdass 3819 tpidm12 3821 diftpsn3 3849 snsstp1 3858 snsstp2 3859 snsstp3 3860 sstp 3870 tpss 3871 dmtpop 5071 2p1e3c 6156 |
Copyright terms: Public domain | W3C validator |