![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmun | Structured version Visualization version GIF version |
Description: The domain of a union is the union of domains. Exercise 56(a) of [Enderton] p. 65. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
dmun | ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unab 4297 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} | |
2 | brun 5198 | . . . . . 6 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) | |
3 | 2 | exbii 1850 | . . . . 5 ⊢ (∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) |
4 | 19.43 1885 | . . . . 5 ⊢ (∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)) | |
5 | 3, 4 | bitr2i 275 | . . . 4 ⊢ ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥) |
6 | 5 | abbii 2802 | . . 3 ⊢ {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
7 | 1, 6 | eqtri 2760 | . 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
8 | df-dm 5685 | . . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} | |
9 | df-dm 5685 | . . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥} | |
10 | 8, 9 | uneq12i 4160 | . 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) |
11 | df-dm 5685 | . 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} | |
12 | 7, 10, 11 | 3eqtr4ri 2771 | 1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 845 = wceq 1541 ∃wex 1781 {cab 2709 ∪ cun 3945 class class class wbr 5147 dom cdm 5675 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-un 3952 df-br 5148 df-dm 5685 |
This theorem is referenced by: rnun 6142 dmpropg 6211 dmtpop 6214 fntpg 6605 fnun 6660 frrlem14 8280 wfrlem13OLD 8317 wfrlem16OLD 8320 tfrlem10 8383 sbthlem5 9083 fodomr 9124 axdc3lem4 10444 hashfun 14393 s4dom 14866 dmtrclfv 14961 strleun 17086 setsdm 17099 estrreslem2 18086 mvdco 19307 gsumzaddlem 19783 cnfldfunALT 20949 cnfldfunALTOLD 20950 noextend 27158 noextendseq 27159 nosupbday 27197 nosupbnd1 27206 nosupbnd2 27208 noinfbday 27212 noinfbnd1 27221 noinfbnd2 27223 noetasuplem4 27228 noetainflem4 27232 uhgrun 28323 upgrun 28367 umgrun 28369 vtxdun 28727 wlkp1 28927 eupthp1 29458 bnj1416 34038 fineqvac 34085 satfdm 34348 fmlasuc0 34363 fixun 34869 rclexi 42351 rtrclex 42353 rtrclexi 42357 cnvrcl0 42361 dmtrcl 42363 dfrtrcl5 42365 dfrcl2 42410 dmtrclfvRP 42466 |
Copyright terms: Public domain | W3C validator |