![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseld | GIF version |
Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.) |
Ref | Expression |
---|---|
sseld.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
sseld | ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseld.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | ssel 3033 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 ⊆ 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-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 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-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-in 3019 df-ss 3026 |
This theorem is referenced by: sselda 3039 sseldd 3040 ssneld 3041 elelpwi 3461 ssbrd 3908 uniopel 4107 onintonm 4362 sucprcreg 4393 ordsuc 4407 0elnn 4460 dmrnssfld 4728 nfunv 5081 opelf 5217 fvimacnv 5453 ffvelrn 5471 resflem 5501 f1imass 5591 dftpos3 6065 nnmordi 6315 mapsn 6487 ixpf 6517 diffifi 6690 ordiso2 6808 prarloclemarch2 7075 ltexprlemrl 7266 cauappcvgprlemladdrl 7313 caucvgprlemladdrl 7334 caucvgprlem1 7335 uzind 8956 supinfneg 9182 infsupneg 9183 ixxssxr 9466 elfz0add 9683 fzoss1 9731 frecuzrdgrclt 9971 fsum3cvg 10936 isumrpcl 11053 lmtopcnp 12117 xmetunirn 12160 mopnval 12244 metrest 12308 bj-nnord 12577 |
Copyright terms: Public domain | W3C validator |