![]() |
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 2917 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | cin 2916 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4, 1 | wceq 1243 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 98 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfss 2932 dfss1 3141 inabs 3168 nssinpss 3169 dfrab3ss 3215 disjssun 3285 riinm 3729 rintm 3744 ssex 3894 op1stb 4209 op1stbg 4210 ssdmres 4633 resima2 4644 xpssres 4645 fnimaeq0 5020 fnreseql 5277 tpostpos2 5880 tfrexlem 5948 ecinxp 6181 uzin 8505 iooval2 8784 bdssex 10022 |
Copyright terms: Public domain | W3C validator |