![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfss2 | Structured version Visualization version 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 3418 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-in 3410 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqeq2i 2462 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | abeq2 2559 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | 3bitri 275 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | pm4.71 635 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 6 | albii 1690 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | bitr4i 256 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-in 3410 df-ss 3417 |
This theorem is referenced by: dfss3 3421 dfss2f 3422 ssel 3425 ssriv 3435 ssrdv 3437 sstr2 3438 eqss 3446 nss 3489 rabss2 3511 ssconb 3565 ssequn1 3603 unss 3607 ssin 3653 reldisj 3807 ssdif0 3822 difin0ss 3832 inssdif0 3833 ssundif 3850 sbcssg 3879 pwss 3965 snss 4095 pwpw0 4119 pwsnALT 4192 ssuni 4219 unissb 4228 intssOLD 4255 iunss 4318 dftr2 4498 axpweq 4579 axpow2 4582 ssextss 4653 ssrel 4922 ssrel2 4924 ssrelrel 4934 reliun 4953 relop 4984 issref 5212 funimass4 5914 dfom2 6691 inf2 8125 grothpw 9248 grothprim 9256 psslinpr 9453 ltaddpr 9456 isprm2 14625 vdwmc2 14922 acsmapd 16417 dfcon2 20427 iskgen3 20557 metcld 22268 metcld2 22269 isch2 26869 pjnormssi 27814 ssiun3 28166 ssrelf 28214 bnj1361 29633 bnj978 29753 dffr5 30386 brsset 30649 sscoid 30673 relowlpssretop 31760 rp-fakeinunass 36154 rababg 36173 ss2iundf 36245 dfss6 36357 dfhe3 36364 snhesn 36376 dffrege76 36529 conss34 36789 sbcssOLD 36901 onfrALTlem2 36906 trsspwALT 37200 trsspwALT2 37201 snssiALTVD 37217 snssiALT 37218 sstrALT2VD 37224 sstrALT2 37225 sbcssgVD 37274 onfrALTlem2VD 37280 sspwimp 37309 sspwimpVD 37310 sspwimpcf 37311 sspwimpcfVD 37312 sspwimpALT 37316 unisnALT 37317 icccncfext 37759 |
Copyright terms: Public domain | W3C validator |