Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ss | Unicode version |
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that (proved in ssid 3087). For a more traditional definition, but requiring a dummy variable, see dfss2 3056. Other possible definitions are given by dfss3 3057, ssequn1 3216, ssequn2 3219, and sseqin2 3265. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
df-ss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | wss 3041 | . 2 |
4 | 1, 2 | cin 3040 | . . 3 |
5 | 4, 1 | wceq 1316 | . 2 |
6 | 3, 5 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfss 3055 dfss1 3250 inabs 3278 dfrab3ss 3324 disjssun 3396 riinm 3855 rintm 3875 ssex 4035 op1stb 4369 op1stbg 4370 ssdmres 4811 resima2 4823 xpssres 4824 fnimaeq0 5214 f0rn0 5287 fnreseql 5498 tpostpos2 6130 tfrexlem 6199 ecinxp 6472 uzin 9314 iooval2 9653 minmax 10956 xrminmax 10989 2prm 11720 dfphi2 11807 restid2 12040 difopn 12188 restopnb 12261 cnrest2 12316 bdssex 12996 |
Copyright terms: Public domain | W3C validator |