![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > difss | GIF 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 3272 | . 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴) | |
2 | 1 | ssriv 3174 | 1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: ∖ cdif 3141 ⊆ wss 3144 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-dif 3146 df-in 3150 df-ss 3157 |
This theorem is referenced by: difssd 3277 difss2 3278 ssdifss 3280 0dif 3509 undif1ss 3512 undifabs 3514 inundifss 3515 undifss 3518 unidif 3856 iunxdif2 3950 difexg 4159 exmid1stab 4226 reldif 4764 cnvdif 5053 resdif 5502 fndmdif 5641 swoer 6586 swoord1 6587 swoord2 6588 phplem2 6880 phpm 6892 unfiin 6953 sbthlem2 6986 sbthlemi4 6988 sbthlemi5 6989 difinfinf 7129 pinn 7337 niex 7340 dmaddpi 7353 dmmulpi 7354 lerelxr 8049 fisumss 11431 fprodssdc 11629 structcnvcnv 12527 strleund 12612 strleun 12613 strle1g 12615 discld 14088 |
Copyright terms: Public domain | W3C validator |