![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > dfss2 | Structured 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 3443 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-in 3435 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqeq2i 2469 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | abeq2 2575 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | 3bitri 271 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | pm4.71 630 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 6 | albii 1611 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | bitr4i 252 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-in 3435 df-ss 3442 |
This theorem is referenced by: dfss3 3446 dfss2f 3447 ssel 3450 ssriv 3460 ssrdv 3462 sstr2 3463 eqss 3471 nss 3514 rabss2 3535 ssconb 3589 ssequn1 3626 unss 3630 ssin 3672 reldisj 3822 ssdif0 3837 difin0ss 3845 inssdif0 3846 ssundif 3862 sbcssg 3890 pwss 3975 snss 4099 pwpw0 4121 pwsnALT 4186 ssuni 4213 unissb 4223 intss 4249 iunss 4311 dftr2 4487 axpweq 4569 axpow2 4572 ssextss 4646 ssrel 5028 ssrel2 5030 ssrelrel 5040 reliun 5060 relop 5090 issref 5311 funimass4 5843 dfom2 6580 inf2 7932 grothpw 9096 grothprim 9104 psslinpr 9303 ltaddpr 9306 isprm2 13875 vdwmc2 14144 acsmapd 15452 bwthOLD 19132 dfcon2 19141 iskgen3 19240 metcld 20934 metcld2 20935 isch2 24763 pjnormssi 25709 ssiun3 26045 ssrelf 26081 dffr5 27699 brsset 28056 sscoid 28080 conss34 29838 clwwlkssclwwlkn 30594 sbcssOLD 31551 onfrALTlem2 31556 trsspwALT 31854 trsspwALT2 31855 snssiALTVD 31865 snssiALT 31866 sstrALT2VD 31872 sstrALT2 31873 sbcssgVD 31921 onfrALTlem2VD 31927 sspwimp 31956 sspwimpVD 31957 sspwimpcf 31958 sspwimpcfVD 31959 sspwimpALT 31963 unisnALT 31964 bnj1361 32124 bnj978 32244 |
Copyright terms: Public domain | W3C validator |