![]() |
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 3141 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | cin 3140 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4, 1 | wceq 1363 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfss 3155 dfss1 3351 inabs 3379 dfrab3ss 3425 disjssun 3498 riinm 3971 rintm 3991 ssex 4152 op1stb 4490 op1stbg 4491 ssdmres 4941 resima2 4953 xpssres 4954 fnimaeq0 5349 f0rn0 5422 fnreseql 5639 tpostpos2 6279 tfrexlem 6348 ecinxp 6623 uzin 9573 iooval2 9928 minmax 11251 xrminmax 11286 2prm 12140 dfphi2 12233 ressbas2d 12541 ressval3d 12545 restid2 12714 lidlbas 13662 difopn 13879 restopnb 13952 cnrest2 14007 bdssex 14925 |
Copyright terms: Public domain | W3C validator |