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 3086 | . . . . . 6 | |
2 | 1 | biimpi 119 | . . . . 5 |
3 | 2 | 19.21bi 1537 | . . . 4 |
4 | 3 | anim2d 335 | . . 3 |
5 | 4 | eximdv 1852 | . 2 |
6 | df-clel 2135 | . 2 | |
7 | df-clel 2135 | . 2 | |
8 | 5, 6, 7 | 3imtr4g 204 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wal 1329 wceq 1331 wex 1468 wcel 1480 wss 3071 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 |
This theorem is referenced by: ssel2 3092 sseli 3093 sseld 3096 sstr2 3104 nelss 3158 ssrexf 3159 ssralv 3161 ssrexv 3162 ralss 3163 rexss 3164 ssconb 3209 sscon 3210 ssdif 3211 unss1 3245 ssrin 3301 difin2 3338 reuss2 3356 reupick 3360 sssnm 3681 uniss 3757 ss2iun 3828 ssiun 3855 iinss 3864 disjss2 3909 disjss1 3912 pwnss 4083 sspwb 4138 ssopab2b 4198 soss 4236 sucssel 4346 ssorduni 4403 onintonm 4433 onnmin 4483 ssnel 4484 wessep 4492 ssrel 4627 ssrel2 4629 ssrelrel 4639 xpss12 4646 cnvss 4712 dmss 4738 elreldm 4765 dmcosseq 4810 relssres 4857 iss 4865 resopab2 4866 issref 4921 ssrnres 4981 dfco2a 5039 cores 5042 funssres 5165 fununi 5191 funimaexglem 5206 dfimafn 5470 funimass4 5472 funimass3 5536 dff4im 5566 funfvima2 5650 funfvima3 5651 f1elima 5674 riotass2 5756 ssoprab2b 5828 resoprab2 5868 releldm2 6083 reldmtpos 6150 dmtpos 6153 rdgss 6280 ss2ixp 6605 fiintim 6817 negf1o 8149 lbreu 8708 lbinf 8711 eqreznegel 9411 negm 9412 iccsupr 9754 negfi 11004 sumrbdclem 11151 prodrbdclem 11345 metrest 12680 bdop 13078 bj-nnen2lp 13157 exmidsbthrlem 13222 |
Copyright terms: Public domain | W3C validator |