![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > undif2 | Structured version Visualization version Unicode version |
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3851). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
undif2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uncom 3590 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | undif1 3854 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | uncom 3590 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3eqtri 2488 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 |
This theorem is referenced by: undif 3860 dfif5 3909 funiunfv 6178 difex2 6625 undom 7686 domss2 7757 sucdom2 7794 unfi 7864 marypha1lem 7973 kmlem11 8616 hashun2 12594 hashun3 12595 cvgcmpce 13927 dprd2da 17724 dpjcntz 17734 dpjdisj 17735 dpjlsm 17736 dpjidcl 17740 ablfac1eu 17755 dfcon2 20483 2ndcdisj2 20521 fixufil 20986 fin1aufil 20996 xrge0gsumle 21900 unmbl 22540 volsup 22558 mbfss 22651 itg2cnlem2 22769 iblss2 22812 amgm 23965 wilthlem2 24043 ftalem3 24048 rpvmasum2 24399 esumpad 28925 imadifss 31973 elrfi 35581 meaunle 38340 |
Copyright terms: Public domain | W3C validator |