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 4420). 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 4128 | . 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴) | |
2 | undif1 4423 | . 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴) | |
3 | uncom 4128 | . 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) | |
4 | 1, 2, 3 | 3eqtri 2848 | 1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∖ cdif 3932 ∪ cun 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 |
This theorem is referenced by: undif 4429 dfif5 4482 funiunfv 7006 difex2 7481 undom 8604 domss2 8675 sucdom2 8713 unfi 8784 marypha1lem 8896 kmlem11 9585 hashun2 13743 hashun3 13744 cvgcmpce 15172 dprd2da 19163 dpjcntz 19173 dpjdisj 19174 dpjlsm 19175 dpjidcl 19179 ablfac1eu 19194 dfconn2 22026 2ndcdisj2 22064 fixufil 22529 fin1aufil 22539 xrge0gsumle 23440 unmbl 24137 volsup 24156 mbfss 24246 itg2cnlem2 24362 iblss2 24405 amgm 25567 wilthlem2 25645 ftalem3 25651 rpvmasum2 26087 esumpad 31314 srcmpltd 32346 noetalem3 33219 noetalem4 33220 imadifss 34866 elrfi 39289 meaunle 42745 |
Copyright terms: Public domain | W3C validator |