New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-ss | GIF version |
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } ⊆ { 1 , 2 , 3 } (ex-ss in set.mm). Note that A ⊆ A (proved in ssid 3290). Contrast this relationship with the relationship A ⊊ B (as will be defined in df-pss 3261). For a more traditional definition, but requiring a dummy variable, see dfss2 3262. Other possible definitions are given by dfss3 3263, dfss4 3489, sspss 3368, ssequn1 3433, ssequn2 3436, sseqin2 3474, and ssdif0 3609. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
df-ss | ⊢ (A ⊆ B ↔ (A ∩ B) = A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | 1, 2 | wss 3257 | . 2 wff A ⊆ B |
4 | 1, 2 | cin 3208 | . . 3 class (A ∩ B) |
5 | 4, 1 | wceq 1642 | . 2 wff (A ∩ B) = A |
6 | 3, 5 | wb 176 | 1 wff (A ⊆ B ↔ (A ∩ B) = A) |
Colors of variables: wff setvar class |
This definition is referenced by: dfss 3260 dfss1 3460 inabs 3486 nssinpss 3487 dfrab3ss 3533 disjssun 3608 riinn0 4040 rintn0 4056 dfiota4 4372 ssfin 4470 ssdmres 4987 resabs1 4992 |
Copyright terms: Public domain | W3C validator |