![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfss4 | Structured version Visualization version Unicode version |
Description: Subclass defined in terms of class difference. See comments under dfun2 3646. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
dfss4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqin2 3619 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eldif 3382 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | notbii 302 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | anbi2i 705 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | elin 3585 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | abai 809 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | iman 430 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 7 | anbi2i 705 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 6, 8 | 3bitri 279 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 4, 9 | bitr4i 260 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10 | difeqri 3521 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | eqeq1i 2457 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 1, 12 | bitr4i 260 |
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 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-v 3015 df-dif 3375 df-in 3379 df-ss 3386 |
This theorem is referenced by: dfin4 3651 sorpsscmpl 6570 sbthlem3 7671 fin23lem7 8733 fin23lem11 8734 compsscnvlem 8787 compssiso 8791 isf34lem4 8794 efgmnvl 17375 frlmlbs 19366 isopn2 20058 iincld 20065 iuncld 20071 clsval2 20076 ntrval2 20077 ntrdif 20078 clsdif 20079 cmclsopn 20088 cmntrcldOLD 20090 opncldf1 20111 indiscld 20118 mretopd 20119 restcld 20199 pnrmopn 20370 conndisj 20442 hausllycmp 20520 kqcldsat 20759 filufint 20946 cfinufil 20954 ufilen 20956 alexsublem 21070 bcth3 22310 inmbl 22507 iccmbl 22531 mbfimaicc 22601 i1fd 22651 itgss3 22784 frgrawopreg2 25791 difuncomp 28177 iundifdifd 28187 iundifdif 28188 cldssbrsiga 29016 unelcarsg 29150 kur14lem4 29938 cldbnd 30988 clsun 30990 mblfinlem3 31981 mblfinlem4 31982 ismblfin 31983 itg2addnclem 31995 fdc 32076 salincl 38241 salexct 38250 ovnsubadd2lem 38530 lincext2 40573 |
Copyright terms: Public domain | W3C validator |