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 3117). For a more traditional definition, but requiring a dummy variable, see dfss2 3086. Other possible definitions are given by dfss3 3087, ssequn1 3246, ssequn2 3249, and sseqin2 3295. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
df-ss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | wss 3071 | . 2 |
4 | 1, 2 | cin 3070 | . . 3 |
5 | 4, 1 | wceq 1331 | . 2 |
6 | 3, 5 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfss 3085 dfss1 3280 inabs 3308 dfrab3ss 3354 disjssun 3426 riinm 3885 rintm 3905 ssex 4065 op1stb 4399 op1stbg 4400 ssdmres 4841 resima2 4853 xpssres 4854 fnimaeq0 5244 f0rn0 5317 fnreseql 5530 tpostpos2 6162 tfrexlem 6231 ecinxp 6504 uzin 9358 iooval2 9698 minmax 11001 xrminmax 11034 2prm 11808 dfphi2 11896 restid2 12129 difopn 12277 restopnb 12350 cnrest2 12405 bdssex 13100 |
Copyright terms: Public domain | W3C validator |