Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dfss2 | Unicode version |
Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) |
Ref | Expression |
---|---|
dfss2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss 3055 | . . 3 | |
2 | df-in 3047 | . . . 4 | |
3 | 2 | eqeq2i 2128 | . . 3 |
4 | abeq2 2226 | . . 3 | |
5 | 1, 3, 4 | 3bitri 205 | . 2 |
6 | pm4.71 386 | . . 3 | |
7 | 6 | albii 1431 | . 2 |
8 | 5, 7 | bitr4i 186 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1314 wceq 1316 wcel 1465 cab 2103 cin 3040 wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: dfss3 3057 dfss2f 3058 ssel 3061 ssriv 3071 ssrdv 3073 sstr2 3074 eqss 3082 nssr 3127 rabss2 3150 ssconb 3179 ssequn1 3216 unss 3220 ssin 3268 ssddif 3280 reldisj 3384 ssdif0im 3397 inssdif0im 3400 ssundifim 3416 sbcssg 3442 pwss 3496 snss 3619 snsssn 3658 ssuni 3728 unissb 3736 intss 3762 iunss 3824 dftr2 3998 axpweq 4065 axpow2 4070 ssextss 4112 ordunisuc2r 4400 setind 4424 zfregfr 4458 tfi 4466 ssrel 4597 ssrel2 4599 ssrelrel 4609 reliun 4630 relop 4659 issref 4891 funimass4 5440 isprm2 11725 bj-inf2vnlem3 13097 bj-inf2vnlem4 13098 |
Copyright terms: Public domain | W3C validator |