Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssdif0 | Structured version Visualization version Unicode version |
Description: Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
ssdif0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iman 440 | . . . 4 | |
2 | eldif 3584 | . . . 4 | |
3 | 1, 2 | xchbinxr 325 | . . 3 |
4 | 3 | albii 1747 | . 2 |
5 | dfss2 3591 | . 2 | |
6 | eq0 3929 | . 2 | |
7 | 4, 5, 6 | 3bitr4i 292 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wa 384 wal 1481 wceq 1483 wcel 1990 cdif 3571 wss 3574 c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-in 3581 df-ss 3588 df-nul 3916 |
This theorem is referenced by: difn0 3943 pssdifn0 3944 difid 3948 vdif0 4037 difrab0eq 4038 difin0 4041 symdifv 4598 wfi 5713 ordintdif 5774 dffv2 6271 fndifnfp 6442 tfi 7053 peano5 7089 wfrlem8 7422 wfrlem16 7430 tz7.49 7540 oe0m1 7601 sdomdif 8108 php3 8146 sucdom2 8156 isinf 8173 unxpwdom2 8493 fin23lem26 9147 fin23lem21 9161 fin1a2lem13 9234 zornn0g 9327 fpwwe2lem13 9464 fpwwe2 9465 isumltss 14580 rpnnen2lem12 14954 symgsssg 17887 symgfisg 17888 psgnunilem5 17914 lspsnat 19145 lsppratlem6 19152 lspprat 19153 lbsextlem4 19161 opsrtoslem2 19485 cnsubrg 19806 0ntr 20875 cmpfi 21211 dfconn2 21222 filconn 21687 cfinfil 21697 ufileu 21723 alexsublem 21848 ptcmplem2 21857 ptcmplem3 21858 restmetu 22375 reconnlem1 22629 bcthlem5 23125 itg10 23455 limcnlp 23642 upgrex 25987 uvtxa01vtx0 26297 ex-dif 27280 strlem1 29109 difininv 29354 difioo 29544 baselcarsg 30368 difelcarsg 30372 sibfof 30402 sitg0 30408 chtvalz 30707 frind 31740 noextendseq 31820 onsucconni 32436 topdifinfeq 33198 fdc 33541 setindtr 37591 relnonrel 37893 caragenunidm 40722 |
Copyright terms: Public domain | W3C validator |