![]() |
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 3118 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-11 1483 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-ext 2136 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1740 df-clab 2141 df-cleq 2147 df-clel 2150 df-in 3104 df-ss 3111 |
This theorem is referenced by: sselda 3124 sseldd 3125 ssneld 3126 elelpwi 3551 ssbrd 4003 uniopel 4211 onintonm 4470 sucprcreg 4502 ordsuc 4516 0elnn 4572 dmrnssfld 4842 nfunv 5196 opelf 5334 fvimacnv 5575 ffvelrn 5593 resflem 5624 f1imass 5715 dftpos3 6199 nnmordi 6452 mapsn 6624 ixpf 6654 diffifi 6828 ordiso2 6965 difinfinf 7031 prarloclemarch2 7318 ltexprlemrl 7509 cauappcvgprlemladdrl 7556 caucvgprlemladdrl 7577 caucvgprlem1 7578 axpre-suploclemres 7800 uzind 9254 supinfneg 9485 infsupneg 9486 ixxssxr 9782 elfz0add 10000 fzoss1 10048 frecuzrdgrclt 10292 fsum3cvg 11252 isumrpcl 11368 fproddccvg 11446 lmtopcnp 12589 txuni2 12595 tx1cn 12608 tx2cn 12609 txlm 12618 imasnopn 12638 xmetunirn 12697 mopnval 12781 metrest 12845 dedekindicc 12950 ivthdec 12961 limcimolemlt 12972 bj-charfundc 13321 bj-nnord 13471 |
Copyright terms: Public domain | W3C validator |