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 3091 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 ⊆ wss 3071 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 |
This theorem is referenced by: sselda 3097 sseldd 3098 ssneld 3099 elelpwi 3522 ssbrd 3971 uniopel 4178 onintonm 4433 sucprcreg 4464 ordsuc 4478 0elnn 4532 dmrnssfld 4802 nfunv 5156 opelf 5294 fvimacnv 5535 ffvelrn 5553 resflem 5584 f1imass 5675 dftpos3 6159 nnmordi 6412 mapsn 6584 ixpf 6614 diffifi 6788 ordiso2 6920 difinfinf 6986 prarloclemarch2 7227 ltexprlemrl 7418 cauappcvgprlemladdrl 7465 caucvgprlemladdrl 7486 caucvgprlem1 7487 axpre-suploclemres 7709 uzind 9162 supinfneg 9390 infsupneg 9391 ixxssxr 9683 elfz0add 9900 fzoss1 9948 frecuzrdgrclt 10188 fsum3cvg 11147 isumrpcl 11263 fproddccvg 11341 lmtopcnp 12419 txuni2 12425 tx1cn 12438 tx2cn 12439 txlm 12448 imasnopn 12468 xmetunirn 12527 mopnval 12611 metrest 12675 dedekindicc 12780 ivthdec 12791 limcimolemlt 12802 bj-nnord 13156 |
Copyright terms: Public domain | W3C validator |