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 3080 | . . 3 | |
2 | df-in 3072 | . . . 4 | |
3 | 2 | eqeq2i 2148 | . . 3 |
4 | abeq2 2246 | . . 3 | |
5 | 1, 3, 4 | 3bitri 205 | . 2 |
6 | pm4.71 386 | . . 3 | |
7 | 6 | albii 1446 | . 2 |
8 | 5, 7 | bitr4i 186 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1329 wceq 1331 wcel 1480 cab 2123 cin 3065 wss 3066 |
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 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-in 3072 df-ss 3079 |
This theorem is referenced by: dfss3 3082 dfss2f 3083 ssel 3086 ssriv 3096 ssrdv 3098 sstr2 3099 eqss 3107 nssr 3152 rabss2 3175 ssconb 3204 ssequn1 3241 unss 3245 ssin 3293 ssddif 3305 reldisj 3409 ssdif0im 3422 inssdif0im 3425 ssundifim 3441 sbcssg 3467 pwss 3521 snss 3644 snsssn 3683 ssuni 3753 unissb 3761 intss 3787 iunss 3849 dftr2 4023 axpweq 4090 axpow2 4095 ssextss 4137 ordunisuc2r 4425 setind 4449 zfregfr 4483 tfi 4491 ssrel 4622 ssrel2 4624 ssrelrel 4634 reliun 4655 relop 4684 issref 4916 funimass4 5465 isprm2 11787 bj-inf2vnlem3 13159 bj-inf2vnlem4 13160 |
Copyright terms: Public domain | W3C validator |