![]() |
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 ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-ss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | wss 2984 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | cin 2983 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4, 1 | wceq 1285 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfss 2998 dfss1 3188 inabs 3215 dfrab3ss 3260 disjssun 3328 riinm 3776 rintm 3791 ssex 3941 op1stb 4262 op1stbg 4263 ssdmres 4691 resima2 4702 xpssres 4703 fnimaeq0 5087 f0rn0 5152 fnreseql 5353 tpostpos2 5961 tfrexlem 6030 ecinxp 6296 uzin 8945 iooval2 9227 minmax 10485 2prm 10888 dfphi2 10975 bdssex 11135 |
Copyright terms: Public domain | W3C validator |