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 3125 | . . 3 | |
2 | df-in 3117 | . . . 4 | |
3 | 2 | eqeq2i 2175 | . . 3 |
4 | abeq2 2273 | . . 3 | |
5 | 1, 3, 4 | 3bitri 205 | . 2 |
6 | pm4.71 387 | . . 3 | |
7 | 6 | albii 1457 | . 2 |
8 | 5, 7 | bitr4i 186 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1340 wceq 1342 wcel 2135 cab 2150 cin 3110 wss 3111 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: dfss3 3127 dfss2f 3128 ssel 3131 ssriv 3141 ssrdv 3143 sstr2 3144 eqss 3152 nssr 3197 rabss2 3220 ssconb 3250 ssequn1 3287 unss 3291 ssin 3339 ssddif 3351 reldisj 3455 ssdif0im 3468 inssdif0im 3471 ssundifim 3487 sbcssg 3513 pwss 3569 snss 3696 snsssn 3735 ssuni 3805 unissb 3813 intss 3839 iunss 3901 dftr2 4076 axpweq 4144 axpow2 4149 ssextss 4192 ordunisuc2r 4485 setind 4510 zfregfr 4545 tfi 4553 ssrel 4686 ssrel2 4688 ssrelrel 4698 reliun 4719 relop 4748 issref 4980 funimass4 5531 isprm2 12028 bj-inf2vnlem3 13695 bj-inf2vnlem4 13696 |
Copyright terms: Public domain | W3C validator |