![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > difss | Unicode version |
Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
difss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifi 3095 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ssriv 3004 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-dif 2976 df-in 2980 df-ss 2987 |
This theorem is referenced by: difssd 3100 difss2 3101 ssdifss 3103 0dif 3316 undif1ss 3319 undifabs 3321 inundifss 3322 undifss 3324 unidif 3635 iunxdif2 3728 difexg 3921 reldif 4479 cnvdif 4754 resdif 5173 fndmdif 5298 swoer 6193 swoord1 6194 swoord2 6195 phplem2 6378 phpm 6390 unfiin 6434 pinn 6550 niex 6553 dmaddpi 6566 dmmulpi 6567 lerelxr 7231 |
Copyright terms: Public domain | W3C validator |