![]() |
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 2911 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | cin 2910 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4, 1 | wceq 1242 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 98 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfss 2926 dfss1 3135 inabs 3162 nssinpss 3163 dfrab3ss 3209 disjssun 3279 riinm 3720 rintm 3735 ssex 3885 op1stb 4175 op1stbg 4176 ssdmres 4576 resima2 4587 xpssres 4588 fnimaeq0 4963 fnreseql 5220 tpostpos2 5821 tfrexlem 5889 ecinxp 6117 uzin 8281 iooval2 8554 bdssex 9357 |
Copyright terms: Public domain | W3C validator |