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 3141 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ 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: sselda 3147 sseldd 3148 ssneld 3149 elelpwi 3576 ssbrd 4030 uniopel 4239 onintonm 4499 sucprcreg 4531 ordsuc 4545 0elnn 4601 dmrnssfld 4872 nfunv 5229 opelf 5367 fvimacnv 5608 ffvelrn 5626 resflem 5657 f1imass 5750 dftpos3 6238 nnmordi 6492 mapsn 6664 ixpf 6694 diffifi 6868 ordiso2 7008 difinfinf 7074 prarloclemarch2 7368 ltexprlemrl 7559 cauappcvgprlemladdrl 7606 caucvgprlemladdrl 7627 caucvgprlem1 7628 axpre-suploclemres 7850 uzind 9310 supinfneg 9541 infsupneg 9542 ixxssxr 9844 elfz0add 10063 fzoss1 10114 frecuzrdgrclt 10358 fsum3cvg 11328 isumrpcl 11444 fproddccvg 11522 reumodprminv 12194 lmtopcnp 12965 txuni2 12971 tx1cn 12984 tx2cn 12985 txlm 12994 imasnopn 13014 xmetunirn 13073 mopnval 13157 metrest 13221 dedekindicc 13326 ivthdec 13337 limcimolemlt 13348 bj-charfundc 13765 bj-nnord 13915 |
Copyright terms: Public domain | W3C validator |