![]() |
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 3159 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 120 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.21bi 1569 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | anim2d 337 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | eximdv 1891 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | df-clel 2185 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | df-clel 2185 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | 3imtr4g 205 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: ssel2 3165 sseli 3166 sseld 3169 sstr2 3177 nelss 3231 ssrexf 3232 ssralv 3234 ssrexv 3235 ralss 3236 rexss 3237 ssconb 3283 sscon 3284 ssdif 3285 unss1 3319 ssrin 3375 difin2 3412 reuss2 3430 reupick 3434 sssnm 3769 uniss 3845 ss2iun 3916 ssiun 3943 iinss 3953 disjss2 3998 disjss1 4001 pwnss 4177 sspwb 4234 ssopab2b 4294 soss 4332 sucssel 4442 ssorduni 4504 onintonm 4534 onnmin 4585 ssnel 4586 wessep 4595 ssrel 4732 ssrel2 4734 ssrelrel 4744 xpss12 4751 cnvss 4818 dmss 4844 elreldm 4871 dmcosseq 4916 relssres 4963 iss 4971 resopab2 4972 issref 5029 ssrnres 5089 dfco2a 5147 cores 5150 funssres 5277 fununi 5303 funimaexglem 5318 dfimafn 5584 funimass4 5586 funimass3 5652 dff4im 5682 funfvima2 5769 funfvima3 5770 f1elima 5794 riotass2 5877 ssoprab2b 5952 resoprab2 5992 releldm2 6209 reldmtpos 6277 dmtpos 6280 rdgss 6407 ss2ixp 6736 fiintim 6956 negf1o 8368 lbreu 8931 lbinf 8934 eqreznegel 9643 negm 9644 iccsupr 9995 negfi 11267 sumrbdclem 11416 prodrbdclem 11610 fprodmodd 11680 mulgpropdg 13101 subgintm 13134 subrngintm 13556 subrgintm 13587 islssm 13670 lspsnel6 13721 islidlm 13792 metrest 14458 bdop 15080 bj-nnen2lp 15159 exmidsbthrlem 15224 |
Copyright terms: Public domain | W3C validator |