Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sseld | Unicode 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 3061 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: sselda 3067 sseldd 3068 ssneld 3069 elelpwi 3492 ssbrd 3941 uniopel 4148 onintonm 4403 sucprcreg 4434 ordsuc 4448 0elnn 4502 dmrnssfld 4772 nfunv 5126 opelf 5264 fvimacnv 5503 ffvelrn 5521 resflem 5552 f1imass 5643 dftpos3 6127 nnmordi 6380 mapsn 6552 ixpf 6582 diffifi 6756 ordiso2 6888 difinfinf 6954 prarloclemarch2 7195 ltexprlemrl 7386 cauappcvgprlemladdrl 7433 caucvgprlemladdrl 7454 caucvgprlem1 7455 axpre-suploclemres 7677 uzind 9130 supinfneg 9358 infsupneg 9359 ixxssxr 9651 elfz0add 9868 fzoss1 9916 frecuzrdgrclt 10156 fsum3cvg 11114 isumrpcl 11231 lmtopcnp 12346 txuni2 12352 tx1cn 12365 tx2cn 12366 txlm 12375 imasnopn 12395 xmetunirn 12454 mopnval 12538 metrest 12602 dedekindicc 12707 ivthdec 12718 limcimolemlt 12729 bj-nnord 13083 |
Copyright terms: Public domain | W3C validator |