![]() |
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 3076 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | cin 3075 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4, 1 | wceq 1332 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfss 3090 dfss1 3285 inabs 3313 dfrab3ss 3359 disjssun 3431 riinm 3893 rintm 3913 ssex 4073 op1stb 4407 op1stbg 4408 ssdmres 4849 resima2 4861 xpssres 4862 fnimaeq0 5252 f0rn0 5325 fnreseql 5538 tpostpos2 6170 tfrexlem 6239 ecinxp 6512 uzin 9382 iooval2 9728 minmax 11033 xrminmax 11066 2prm 11844 dfphi2 11932 restid2 12168 difopn 12316 restopnb 12389 cnrest2 12444 bdssex 13271 |
Copyright terms: Public domain | W3C validator |