Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > difun2 | Structured version Visualization version Unicode version |
Description: Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
difun2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difundir 3880 | . 2 | |
2 | difid 3948 | . . 3 | |
3 | 2 | uneq2i 3764 | . 2 |
4 | un0 3967 | . 2 | |
5 | 1, 3, 4 | 3eqtri 2648 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 cdif 3571 cun 3572 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-ral 2917 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 |
This theorem is referenced by: uneqdifeq 4057 uneqdifeqOLD 4058 difprsn1 4330 orddif 5820 domunsncan 8060 elfiun 8336 hartogslem1 8447 cantnfp1lem3 8577 cda1dif 8998 infcda1 9015 ssxr 10107 dfn2 11305 incexclem 14568 mreexmrid 16303 lbsextlem4 19161 ufprim 21713 volun 23313 i1f1 23457 itgioo 23582 itgsplitioo 23604 plyeq0lem 23966 jensen 24715 difeq 29355 fzdif2 29551 fzodif2 29552 measun 30274 carsgclctunlem1 30379 carsggect 30380 chtvalz 30707 elmrsubrn 31417 mrsubvrs 31419 finixpnum 33394 lindsenlbs 33404 poimirlem2 33411 poimirlem4 33413 poimirlem6 33415 poimirlem7 33416 poimirlem8 33417 poimirlem11 33420 poimirlem12 33421 poimirlem13 33422 poimirlem14 33423 poimirlem16 33425 poimirlem18 33427 poimirlem19 33428 poimirlem21 33430 poimirlem23 33432 poimirlem27 33436 poimirlem30 33439 asindmre 33495 kelac2 37635 pwfi2f1o 37666 iccdifioo 39741 iccdifprioo 39742 hoiprodp1 40802 |
Copyright terms: Public domain | W3C validator |