![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elun1 | GIF version |
Description: Membership law for union of classes. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
elun1 | ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 3178 | . 2 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶) | |
2 | 1 | sseli 3035 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 ∪ cun 3011 |
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 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-un 3017 df-in 3019 df-ss 3026 |
This theorem is referenced by: dcun 3412 exmidundif 4058 exmidundifim 4059 brtposg 6057 dftpos4 6066 dcdifsnid 6303 undifdcss 6713 fidcenumlemrks 6742 djulclr 6821 djulcl 6823 djuss 6841 finomni 6883 hashennnuni 10318 sumsplitdc 10990 srngbased 11781 srngplusgd 11782 srngmulrd 11783 lmodbased 11792 lmodplusgd 11793 lmodscad 11794 ipsbased 11800 ipsaddgd 11801 ipsmulrd 11802 |
Copyright terms: Public domain | W3C validator |