New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-ss | Unicode 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 (proved in ssid 3290). Contrast this relationship with the relationship (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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | wss 3257 | . 2 |
4 | 1, 2 | cin 3208 | . . 3 |
5 | 4, 1 | wceq 1642 | . 2 |
6 | 3, 5 | wb 176 | 1 |
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 |