![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > undif2 | Structured version Visualization version GIF version |
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4184). 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 3900 | . 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴) | |
2 | undif1 4187 | . 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴) | |
3 | uncom 3900 | . 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) | |
4 | 1, 2, 3 | 3eqtri 2786 | 1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1632 ∖ cdif 3712 ∪ cun 3713 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 |
This theorem is referenced by: undif 4193 dfif5 4246 funiunfv 6669 difex2 7134 undom 8213 domss2 8284 sucdom2 8321 unfi 8392 marypha1lem 8504 kmlem11 9174 hashun2 13364 hashun3 13365 cvgcmpce 14749 dprd2da 18641 dpjcntz 18651 dpjdisj 18652 dpjlsm 18653 dpjidcl 18657 ablfac1eu 18672 dfconn2 21424 2ndcdisj2 21462 fixufil 21927 fin1aufil 21937 xrge0gsumle 22837 unmbl 23505 volsup 23524 mbfss 23612 itg2cnlem2 23728 iblss2 23771 amgm 24916 wilthlem2 24994 ftalem3 25000 rpvmasum2 25400 esumpad 30426 noetalem3 32171 noetalem4 32172 imadifss 33697 elrfi 37759 meaunle 41184 |
Copyright terms: Public domain | W3C validator |