Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssin | Structured version Visualization version Unicode version |
Description: Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
ssin |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3796 | . . . . 5 | |
2 | 1 | imbi2i 326 | . . . 4 |
3 | 2 | albii 1747 | . . 3 |
4 | jcab 907 | . . . 4 | |
5 | 4 | albii 1747 | . . 3 |
6 | 19.26 1798 | . . 3 | |
7 | 3, 5, 6 | 3bitrri 287 | . 2 |
8 | dfss2 3591 | . . 3 | |
9 | dfss2 3591 | . . 3 | |
10 | 8, 9 | anbi12i 733 | . 2 |
11 | dfss2 3591 | . 2 | |
12 | 7, 10, 11 | 3bitr4i 292 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wal 1481 wcel 1990 cin 3573 wss 3574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 |
This theorem is referenced by: ssini 3836 ssind 3837 uneqin 3878 disjpss 4028 trin 4763 pwin 5018 fin 6085 wfrlem4 7418 epfrs 8607 tcmin 8617 resscntz 17764 subgdmdprd 18433 tgval 20759 eltg3i 20765 innei 20929 cnprest2 21094 subislly 21284 lly1stc 21299 xkohaus 21456 xkoinjcn 21490 opnfbas 21646 supfil 21699 rnelfm 21757 tsmsres 21947 restmetu 22375 chabs2 28376 cmbr4i 28460 pjin3i 29053 mdbr2 29155 dmdbr2 29162 dmdbr5 29167 mdslle1i 29176 mdslle2i 29177 mdslj1i 29178 mdslj2i 29179 mdsl2i 29181 mdslmd1lem1 29184 mdslmd1lem2 29185 mdslmd1i 29188 mdslmd3i 29191 hatomistici 29221 chrelat2i 29224 cvexchlem 29227 mdsymlem1 29262 mdsymlem3 29264 mdsymlem6 29267 dmdbr5ati 29281 pnfneige0 29997 ballotlem2 30550 iccllysconn 31232 frrlem4 31783 heibor1lem 33608 dochexmidlem1 36749 superficl 37872 k0004lem1 38445 |
Copyright terms: Public domain | W3C validator |