![]() |
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 3163 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2159 ⊆ wss 3143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2170 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-sb 1773 df-clab 2175 df-cleq 2181 df-clel 2184 df-in 3149 df-ss 3156 |
This theorem is referenced by: sselda 3169 sseldd 3170 ssneld 3171 elelpwi 3601 ssbrd 4060 uniopel 4270 onintonm 4530 sucprcreg 4562 ordsuc 4576 0elnn 4632 dmrnssfld 4904 nfunv 5263 opelf 5401 fvimacnv 5646 ffvelcdm 5664 resflem 5695 f1imass 5790 dftpos3 6280 nnmordi 6534 mapsn 6707 ixpf 6737 diffifi 6911 ordiso2 7051 difinfinf 7117 exmidapne 7276 prarloclemarch2 7435 ltexprlemrl 7626 cauappcvgprlemladdrl 7673 caucvgprlemladdrl 7694 caucvgprlem1 7695 axpre-suploclemres 7917 uzind 9381 supinfneg 9612 infsupneg 9613 ixxssxr 9917 elfz0add 10137 fzoss1 10188 frecuzrdgrclt 10432 fsum3cvg 11403 isumrpcl 11519 fproddccvg 11597 reumodprminv 12270 issubmnd 12868 issubg2m 13093 eqgid 13130 issubrng2 13517 subrgdvds 13542 issubrg2 13548 lssats2 13690 rnglidlmmgm 13772 rnglidlmsgrp 13773 rnglidlrng 13774 lmtopcnp 14133 txuni2 14139 tx1cn 14152 tx2cn 14153 txlm 14162 imasnopn 14182 xmetunirn 14241 mopnval 14325 metrest 14389 dedekindicc 14494 ivthdec 14505 limcimolemlt 14516 bj-charfundc 14943 bj-nnord 15093 |
Copyright terms: Public domain | W3C validator |