Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssun1 | GIF version |
Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ssun1 | ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc 702 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
2 | elun 3258 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | sylibr 133 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵)) |
4 | 3 | ssriv 3141 | 1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ∨ wo 698 ∈ wcel 2135 ∪ cun 3109 ⊆ wss 3111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-in 3117 df-ss 3124 |
This theorem is referenced by: ssun2 3281 ssun3 3282 elun1 3284 inabs 3349 reuun1 3399 un00 3450 undifabs 3480 undifss 3484 snsspr1 3715 snsstp1 3717 snsstp2 3718 prsstp12 3720 exmidundif 4179 sssucid 4387 unexb 4414 dmexg 4862 fvun1 5546 dftpos2 6220 tpostpos2 6224 ac6sfi 6855 caserel 7043 finomni 7095 ressxr 7933 nnssnn0 9108 un0addcl 9138 un0mulcl 9139 nn0ssxnn0 9171 fsumsplit 11334 fsum2d 11362 fsumabs 11392 fprodsplitdc 11523 fprod2d 11550 ennnfonelemss 12280 bdunexb 13637 |
Copyright terms: Public domain | W3C validator |