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 2988 | . . . . . 6 | |
2 | 1 | biimpi 118 | . . . . 5 |
3 | 2 | 19.21bi 1490 | . . . 4 |
4 | 3 | anim2d 330 | . . 3 |
5 | 4 | eximdv 1801 | . 2 |
6 | df-clel 2077 | . 2 | |
7 | df-clel 2077 | . 2 | |
8 | 5, 6, 7 | 3imtr4g 203 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 wal 1282 wceq 1284 wex 1421 wcel 1433 wss 2973 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-11 1437 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-in 2979 df-ss 2986 |
This theorem is referenced by: ssel2 2994 sseli 2995 sseld 2998 sstr2 3006 ssralv 3058 ssrexv 3059 ralss 3060 rexss 3061 ssconb 3105 sscon 3106 ssdif 3107 unss1 3141 ssrin 3191 difin2 3226 reuss2 3244 reupick 3248 sssnm 3546 uniss 3622 ss2iun 3693 ssiun 3720 iinss 3729 disjss2 3769 disjss1 3772 pwnss 3933 sspwb 3971 ssopab2b 4031 soss 4069 sucssel 4179 ssorduni 4231 onintonm 4261 onnmin 4311 ssnel 4312 wessep 4320 ssrel 4446 ssrel2 4448 ssrelrel 4458 xpss12 4463 cnvss 4526 dmss 4552 elreldm 4578 dmcosseq 4621 relssres 4666 iss 4674 resopab2 4675 issref 4727 ssrnres 4783 dfco2a 4841 cores 4844 funssres 4962 fununi 4987 funimaexglem 5002 dfimafn 5243 funimass4 5245 funimass3 5304 dff4im 5334 funfvima2 5412 funfvima3 5413 f1elima 5433 riotass2 5514 ssoprab2b 5582 resoprab2 5618 releldm2 5831 reldmtpos 5891 dmtpos 5894 rdgss 5993 negf1o 7486 lbreu 8023 lbinf 8026 eqreznegel 8699 negm 8700 iccsupr 8989 negfi 10110 bdop 10666 bj-nnen2lp 10749 |
Copyright terms: Public domain | W3C validator |