![]() |
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 669 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
2 | elun 3144 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | sylibr 133 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵)) |
4 | 3 | ssriv 3032 | 1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ∨ wo 665 ∈ wcel 1439 ∪ cun 3000 ⊆ wss 3002 |
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-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-v 2624 df-un 3006 df-in 3008 df-ss 3015 |
This theorem is referenced by: ssun2 3167 ssun3 3168 elun1 3170 inabs 3234 reuun1 3284 un00 3335 undifabs 3365 undifss 3369 snsspr1 3593 snsstp1 3595 snsstp2 3596 prsstp12 3598 exmidundif 4045 sssucid 4253 unexb 4279 dmexg 4712 fvun1 5385 dftpos2 6042 tpostpos2 6046 ac6sfi 6670 caserel 6834 finomni 6859 ressxr 7594 nnssnn0 8739 un0addcl 8769 un0mulcl 8770 nn0ssxnn0 8802 fsumsplit 10864 fsum2d 10892 fsumabs 10922 bdunexb 12115 |
Copyright terms: Public domain | W3C validator |