![]() |
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 3137 | . 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴) | |
2 | 1 | ssriv 3043 | 1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: ∖ cdif 3010 ⊆ wss 3013 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-dif 3015 df-in 3019 df-ss 3026 |
This theorem is referenced by: difssd 3142 difss2 3143 ssdifss 3145 0dif 3373 undif1ss 3376 undifabs 3378 inundifss 3379 undifss 3382 unidif 3707 iunxdif2 3800 difexg 4001 reldif 4587 cnvdif 4871 resdif 5310 fndmdif 5443 swoer 6360 swoord1 6361 swoord2 6362 phplem2 6649 phpm 6661 unfiin 6716 sbthlem2 6747 sbthlemi4 6749 sbthlemi5 6750 pinn 6965 niex 6968 dmaddpi 6981 dmmulpi 6982 lerelxr 7646 fisumss 10935 structcnvcnv 11659 strleund 11731 strleun 11732 strle1g 11733 discld 11988 |
Copyright terms: Public domain | W3C validator |