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 4411). 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 4092 | . 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴) | |
2 | undif1 4415 | . 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴) | |
3 | uncom 4092 | . 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) | |
4 | 1, 2, 3 | 3eqtri 2772 | 1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∖ cdif 3889 ∪ cun 3890 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 |
This theorem is referenced by: undif 4421 dfif5 4481 funiunfv 7116 difex2 7602 undom 8821 sucdom2 8843 domss2 8897 unfiOLD 9051 marypha1lem 9162 kmlem11 9909 hashun2 14088 hashun3 14089 cvgcmpce 15520 dprd2da 19635 dpjcntz 19645 dpjdisj 19646 dpjlsm 19647 dpjidcl 19651 ablfac1eu 19666 dfconn2 22560 2ndcdisj2 22598 fixufil 23063 fin1aufil 23073 xrge0gsumle 23986 unmbl 24691 volsup 24710 mbfss 24800 itg2cnlem2 24917 iblss2 24960 amgm 26130 wilthlem2 26208 ftalem3 26214 rpvmasum2 26650 esumpad 32011 srcmpltd 33042 noetasuplem4 33927 noetainflem4 33931 imadifss 35740 elrfi 40505 meaunle 43965 |
Copyright terms: Public domain | W3C validator |