Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssel2 | GIF version |
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.) |
Ref | Expression |
---|---|
ssel2 | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3141 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
2 | 1 | imp 123 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2141 ⊆ wss 3121 |
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-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 |
This theorem is referenced by: elnn 4588 funimass4 5545 fvelimab 5550 ssimaex 5555 funconstss 5611 rexima 5731 ralima 5732 1st2nd 6157 f1o2ndf1 6204 tfri1dALT 6327 eldju1st 7044 axsuploc 7979 lbinf 8851 dfinfre 8859 lbzbi 9562 elfzom1elp1fzo 10145 ssfzo12 10167 seq3split 10422 shftlem 10767 uzwodc 11979 tgcl 12779 neipsm 12869 txbasval 12982 elmopn2 13164 metrest 13221 cncfmet 13294 negcncf 13303 reeff1olem 13407 |
Copyright terms: Public domain | W3C validator |