![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssel | Unicode version |
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ssel |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 3036 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 119 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.21bi 1505 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | anim2d 333 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | eximdv 1819 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | df-clel 2096 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | df-clel 2096 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | 3imtr4g 204 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-11 1452 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-in 3027 df-ss 3034 |
This theorem is referenced by: ssel2 3042 sseli 3043 sseld 3046 sstr2 3054 ssralv 3108 ssrexv 3109 ralss 3110 rexss 3111 ssconb 3156 sscon 3157 ssdif 3158 unss1 3192 ssrin 3248 difin2 3285 reuss2 3303 reupick 3307 sssnm 3628 uniss 3704 ss2iun 3775 ssiun 3802 iinss 3811 disjss2 3855 disjss1 3858 pwnss 4023 sspwb 4076 ssopab2b 4136 soss 4174 sucssel 4284 ssorduni 4341 onintonm 4371 onnmin 4421 ssnel 4422 wessep 4430 ssrel 4565 ssrel2 4567 ssrelrel 4577 xpss12 4584 cnvss 4650 dmss 4676 elreldm 4703 dmcosseq 4746 relssres 4793 iss 4801 resopab2 4802 issref 4857 ssrnres 4917 dfco2a 4975 cores 4978 funssres 5101 fununi 5127 funimaexglem 5142 dfimafn 5402 funimass4 5404 funimass3 5468 dff4im 5498 funfvima2 5582 funfvima3 5583 f1elima 5606 riotass2 5688 ssoprab2b 5760 resoprab2 5800 releldm2 6013 reldmtpos 6080 dmtpos 6083 rdgss 6210 ss2ixp 6535 fiintim 6746 negf1o 8011 lbreu 8561 lbinf 8564 eqreznegel 9256 negm 9257 iccsupr 9590 negfi 10838 sumrbdclem 10984 metrest 12434 bdop 12654 bj-nnen2lp 12737 exmidsbthrlem 12801 |
Copyright terms: Public domain | W3C validator |